< 1625530613 951212 :Lord_of_Life!~Lord@user/lord-of-life/x-2819915 QUIT :Read error: Connection reset by peer < 1625530752 32705 :Lord_of_Life!~Lord@user/lord-of-life/x-2819915 JOIN :#esolangs < 1625533900 399638 :dbohdan!~dbohdan@user/dbohdan QUIT :Quit: ZNC 1.7.2+deb3 - https://znc.in < 1625533912 536588 :dbohdan!~dbohdan@user/dbohdan JOIN :#esolangs < 1625537452 175442 :nakilon!~nakilon@user/nakilon PRIVMSG #esolangs :did another approach but it's much slower ( https://i.imgur.com/uMvEce9.png < 1625540916 571519 :aquijoule_!~richbridg@213-225-13-36.nat.highway.a1.net JOIN :#esolangs < 1625541052 653028 :richbridger!~richbridg@213-225-32-103.nat.highway.a1.net QUIT :Ping timeout: 246 seconds > 1625541156 278448 PRIVMSG #esolangs :14[[07Py25614]]4 M10 02https://esolangs.org/w/index.php?diff=85773&oldid=84554 5* 03Makonede 5* (+16) 10 < 1625542996 173625 :monoxane!~monoxane@119-18-17-227.771211.mel.static.aussiebb.net QUIT :Quit: estoy fuera < 1625543028 200926 :monoxane!~monoxane@119-18-17-227.771211.mel.static.aussiebb.net JOIN :#esolangs > 1625543937 864586 PRIVMSG #esolangs :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=85774&oldid=85748 5* 03BurningApparatus 5* (+201) 10/* Introductions */ < 1625547664 969588 :nakilon!~nakilon@user/nakilon PRIVMSG #esolangs :https://i.imgur.com/vqjmZFl.mp4 < 1625549708 215705 :monoxane!~monoxane@119-18-17-227.771211.mel.static.aussiebb.net QUIT :Quit: estoy fuera < 1625549740 330264 :monoxane!~monoxane@119-18-17-227.771211.mel.static.aussiebb.net JOIN :#esolangs < 1625553415 739634 :nakilon!~nakilon@user/nakilon PRIVMSG #esolangs :https://i.imgur.com/7L3ELnH.mp4 < 1625555777 767510 :Sgeo!~Sgeo@user/sgeo QUIT :Read error: Connection reset by peer < 1625558451 880658 :riv!~river@tilde.team/user/river QUIT :Quit: Leaving < 1625558794 812375 :hendursa1!~weechat@user/hendursaga JOIN :#esolangs < 1625558987 830153 :hendursaga!~weechat@user/hendursaga QUIT :Ping timeout: 244 seconds < 1625559707 644698 :Lord_of_Life_!~Lord@user/lord-of-life/x-2819915 JOIN :#esolangs < 1625559729 171718 :Lord_of_Life!~Lord@user/lord-of-life/x-2819915 QUIT :Ping timeout: 252 seconds < 1625559866 761482 :Lord_of_Life_!~Lord@user/lord-of-life/x-2819915 NICK :Lord_of_Life < 1625561089 531038 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esolangs :Hmm, is the infinite variant of Lagrange's group theory theorem equivalent to the axiom of choice? > 1625561195 240035 PRIVMSG #esolangs :14[[07Special:Log/newusers14]]4 create10 02 5* 03Flyingmadpakke 5* 10New user account < 1625561378 324641 :Corbin!~Corbin@c-73-67-140-116.hsd1.or.comcast.net PRIVMSG #esolangs :It feels like it. It seems plausible that Lagrange's theorem requires LEM (which implies AOC) just to choose equivalence classes and take subgroups, but I'm not sure. The other direction seems easy enough. < 1625562555 87982 :int-e!~noone@int-e.eu PRIVMSG #esolangs :"LEM (which implies AOC)"... no < 1625562652 942652 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esolangs :Yeah, AOC => LEM but not the other way around, I'm pretty sure < 1625562902 675731 :int-e!~noone@int-e.eu PRIVMSG #esolangs :I'm trying to remember how AOC implies LEM. Ah, you can let A = {0 | P} u {1 | ~P}, prove that A != {}, and then AOC picks an element of the sole element of X = {A} and that'll tell you which of P or ~P is true. < 1625562991 225545 :int-e!~noone@int-e.eu PRIVMSG #esolangs :So it seems to be a quirk of encoding emptiness as {} \notin X rather than the positive assertion that forall A in X, exists a in A, true < 1625563029 699636 :int-e!~noone@int-e.eu PRIVMSG #esolangs :err, encoding the fact that the sets in X are non-empty < 1625563177 807130 :hanif!~hanif@gateway/tor-sasl/hanif JOIN :#esolangs < 1625563225 766884 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esolangs :https://en.wikipedia.org/wiki/Diaconescu%27s_theorem I think < 1625563268 887499 :Corbin!~Corbin@c-73-67-140-116.hsd1.or.comcast.net PRIVMSG #esolangs :You're entirely correct. < 1625563567 592781 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Ah, that's a bit more clever... we *can* exhibit elements of U and V there, so it's not just an encoding quirk. < 1625563595 53326 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Taneb: thanks < 1625563691 125847 :shachaf!~shachaf@user/shachaf PRIVMSG #esolangs :I heard about the axiom of global choice recently. What a great axiom. < 1625563820 932855 :int-e!~noone@int-e.eu PRIVMSG #esolangs :what's next? epsilon calculus? < 1625563894 561660 :shachaf!~shachaf@user/shachaf PRIVMSG #esolangs :Ah, I hadn't heard of that either. < 1625563899 541478 :Koen!~Koen@92.167.9.109.rev.sfr.net JOIN :#esolangs < 1625563929 246008 :shachaf!~shachaf@user/shachaf PRIVMSG #esolangs :This epsilon thing is slightly reminiscent of "seemingly impossible programs". < 1625563965 535326 :shachaf!~shachaf@user/shachaf PRIVMSG #esolangs :Where the find operator also takes a predicate and returns a value that satisfies it, if it exists, or otherwise an unspecified value. < 1625563974 740736 :shachaf!~shachaf@user/shachaf PRIVMSG #esolangs :And exists and forall are implemented the same way. < 1625564056 483863 :shachaf!~shachaf@user/shachaf PRIVMSG #esolangs :Maybe this epsilon thing works well in some sort of compactness-related context. < 1625564076 584965 :shachaf!~shachaf@user/shachaf PRIVMSG #esolangs :Hmm, I still don't really know what the computational content of compactness is, in that sort of context. < 1625566341 471796 :arseniiv!~arseniiv@94.41.6.151.dynamic.ufanet.ru JOIN :#esolangs < 1625569793 806704 :Koen!~Koen@92.167.9.109.rev.sfr.net QUIT :Remote host closed the connection < 1625570174 398964 :Koen!~Koen@92.167.9.109.rev.sfr.net JOIN :#esolangs < 1625571031 428200 :Koen!~Koen@92.167.9.109.rev.sfr.net QUIT :Remote host closed the connection < 1625572269 533647 :Koen!~Koen@92.167.9.109.rev.sfr.net JOIN :#esolangs < 1625572534 707663 :hanif!~hanif@gateway/tor-sasl/hanif QUIT :Ping timeout: 244 seconds < 1625573379 436231 :tromp!~textual@dhcp-077-249-230-040.chello.nl JOIN :#esolangs < 1625575418 775447 :hanif!~hanif@gateway/tor-sasl/hanif JOIN :#esolangs < 1625575811 435035 :velik!~velik@62.241.154.104.bc.googleusercontent.com QUIT :Remote host closed the connection < 1625579767 454775 :Sgeo!~Sgeo@user/sgeo JOIN :#esolangs < 1625579881 776661 :hanif!~hanif@gateway/tor-sasl/hanif QUIT :Ping timeout: 244 seconds < 1625582506 479834 :arseniiv!~arseniiv@94.41.6.151.dynamic.ufanet.ru QUIT :Ping timeout: 240 seconds > 1625583516 368728 PRIVMSG #esolangs :14[[07Language list14]]4 M10 02https://esolangs.org/w/index.php?diff=85775&oldid=85749 5* 03PythonshellDebugwindow 5* (+12) 10/* R */ RHOVL > 1625583617 768230 PRIVMSG #esolangs :14[[07RHOVL14]]4 M10 02https://esolangs.org/w/index.php?diff=85776&oldid=85760 5* 03PythonshellDebugwindow 5* (+78) 10/* Interpreter */ Cats > 1625583652 843589 PRIVMSG #esolangs :14[[07RHOVL14]]4 M10 02https://esolangs.org/w/index.php?diff=85777&oldid=85776 5* 03PythonshellDebugwindow 5* (+70) 10Refimpl > 1625585538 46949 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85778&oldid=70408 5* 03Dtuser1337 5* (+1474) 10/* Beginning of the Sandbox line */ < 1625586587 801782 :Koen!~Koen@92.167.9.109.rev.sfr.net QUIT :Remote host closed the connection < 1625586850 963216 :riv!~river@tilde.team/user/river JOIN :#esolangs < 1625587255 605115 :delta23!~delta23@user/delta23 JOIN :#esolangs > 1625587517 238601 PRIVMSG #esolangs :14[[07Talk:Cheese14]]4 10 02https://esolangs.org/w/index.php?diff=85779&oldid=85200 5* 03Sanscicondos 5* (+53) 10/* Know Bugs As of Version [Alpha 1.3] */ < 1625588137 819630 :hanif!~hanif@gateway/tor-sasl/hanif JOIN :#esolangs > 1625588180 886065 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85780&oldid=85778 5* 03Dtuser1337 5* (+569) 10/* Commands */ < 1625588504 118287 :tromp!~textual@dhcp-077-249-230-040.chello.nl QUIT :Read error: Connection reset by peer < 1625588715 619050 :nakilon!~nakilon@user/nakilon PRIVMSG #esolangs :https://i.imgur.com/y3Tg3oj.png ; https://i.imgur.com/O5sSCPR.mp4 < 1625589114 326054 :leah2!~leah@vuxu.org QUIT :Ping timeout: 240 seconds < 1625589157 948608 :nakilon!~nakilon@user/nakilon PRIVMSG #esolangs :https://i.imgur.com/yBhtVxG.png ; https://i.imgur.com/19kdpY0.mp4 < 1625589289 452966 :leah2!~leah@vuxu.org JOIN :#esolangs < 1625589584 696805 :hanif!~hanif@gateway/tor-sasl/hanif QUIT :Ping timeout: 244 seconds < 1625590324 468952 :arseniiv!~arseniiv@94.41.6.151.dynamic.ufanet.ru JOIN :#esolangs > 1625591175 436867 PRIVMSG #esolangs :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=85781&oldid=85774 5* 03Flyingmadpakke 5* (+151) 10/* Introductions */ > 1625591413 752530 PRIVMSG #esolangs :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=85782&oldid=85781 5* 03Flyingmadpakke 5* (+81) 10/* Introductions */ < 1625593434 765877 :hanif!~hanif@gateway/tor-sasl/hanif JOIN :#esolangs > 1625594964 928375 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85783&oldid=85780 5* 03Dtuser1337 5* (+2759) 10/* Commands */ > 1625595001 751898 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85784&oldid=85783 5* 03Dtuser1337 5* (+7) 10/* Commands */ < 1625595024 787122 :nakilon!~nakilon@user/nakilon PRIVMSG #esolangs :heh, while small objects like this crater go well https://i.imgur.com/pHR2Fse.png > 1625595038 38831 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85785&oldid=85784 5* 03Dtuser1337 5* (+0) 10/* Commands */ < 1625595049 909118 :nakilon!~nakilon@user/nakilon PRIVMSG #esolangs :this one does not ( https://i.imgur.com/NfwEnKO.png > 1625595078 61171 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85786&oldid=85785 5* 03Dtuser1337 5* (-3) 10/* Commands */ < 1625595107 801205 :nakilon!~nakilon@user/nakilon PRIVMSG #esolangs :oh < 1625595137 948611 :nakilon!~nakilon@user/nakilon PRIVMSG #esolangs :I imagine I could generate the image on lower resolution and then recursively go 2 times higher < 1625595152 814806 :nakilon!~nakilon@user/nakilon PRIVMSG #esolangs :but it's too complex compared to current state > 1625595466 209045 PRIVMSG #esolangs :14[[07Talk:Truth-machine14]]4 10 02https://esolangs.org/w/index.php?diff=85787&oldid=77361 5* 03Flyingmadpakke 5* (+1507) 10 < 1625595967 544722 :Oshawott!~archenoth@S0106889e6827f474.cg.shawcable.net QUIT :Ping timeout: 246 seconds < 1625596067 223035 :hanif!~hanif@gateway/tor-sasl/hanif QUIT :Quit: quit > 1625596334 564804 PRIVMSG #esolangs :14[[07\ () /14]]4 10 02https://esolangs.org/w/index.php?diff=85788&oldid=81658 5* 03LegionMammal978 5* (+226) 10fix links > 1625597633 380486 PRIVMSG #esolangs :14[[07DROL14]]4 10 02https://esolangs.org/w/index.php?diff=85789&oldid=81673 5* 03LegionMammal978 5* (+10) 10/* External Links */ fix links < 1625597924 737501 :nakilon!~nakilon@user/nakilon PRIVMSG #esolangs :I guess I'll stop on this for now > 1625598162 66778 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85790&oldid=85786 5* 03Dtuser1337 5* (+1826) 10/* Commands */ > 1625598741 111982 PRIVMSG #esolangs :14[[07Shove14]]4 M10 02https://esolangs.org/w/index.php?diff=85791&oldid=44005 5* 03OrichalcumCosmonaut 5* (-13) 10fix spacing of and un-preformat the space instruction > 1625599158 879245 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85792&oldid=85790 5* 03Dtuser1337 5* (+958) 10/* Commands */ > 1625599503 16165 PRIVMSG #esolangs :14[[07Muddle14]]4 10 02https://esolangs.org/w/index.php?diff=85793&oldid=77988 5* 03LegionMammal978 5* (+8) 10/* Interpreter */ fix links < 1625599658 938480 :imode!~imode@user/imode PRIVMSG #esolangs :is the singingbanana on the esowiki the same singingbanana that does the numberphile videos? > 1625599829 461244 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85794&oldid=85792 5* 03Dtuser1337 5* (+150) 10 > 1625600156 914902 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85795&oldid=85794 5* 03Dtuser1337 5* (+108) 10 > 1625600308 938447 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85796&oldid=85795 5* 03Dtuser1337 5* (+100) 10/* Commands */ > 1625600519 963246 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85797&oldid=85796 5* 03Dtuser1337 5* (-79) 10/* Beginning of the Sandbox line */ > 1625600608 44185 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85798&oldid=85797 5* 03Dtuser1337 5* (+40) 10/* Beginning of the Sandbox line */ > 1625600674 806502 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85799&oldid=85798 5* 03Dtuser1337 5* (-12) 10/* Commands */ > 1625600767 291414 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85800&oldid=85799 5* 03Dtuser1337 5* (+7) 10/* Commands */ > 1625600996 151419 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85801&oldid=85800 5* 03Dtuser1337 5* (+50) 10/* Examples */ > 1625601950 125137 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85802&oldid=85801 5* 03Dtuser1337 5* (+375) 10/* Examples */ > 1625602349 895562 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85803&oldid=85802 5* 03Dtuser1337 5* (+235) 10/* Function Commands */ > 1625602365 460894 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85804&oldid=85803 5* 03Dtuser1337 5* (-1) 10/* Function Commands */ > 1625602511 573802 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85805&oldid=85804 5* 03Dtuser1337 5* (+32) 10/* Function Commands */ > 1625602545 628569 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85806&oldid=85805 5* 03Dtuser1337 5* (-13) 10/* Function Commands */ > 1625602614 69942 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85807&oldid=85806 5* 03Dtuser1337 5* (-11) 10/* Cat */ > 1625602665 811276 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85808&oldid=85807 5* 03Dtuser1337 5* (+30) 10/* File I/O Commands */ > 1625602692 229785 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85809&oldid=85808 5* 03Dtuser1337 5* (+0) 10/* File I/O Commands */ > 1625602713 367750 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85810&oldid=85809 5* 03Dtuser1337 5* (+13) 10/* File I/O Commands */ < 1625602927 965254 :Koen!~Koen@92.167.9.109.rev.sfr.net JOIN :#esolangs < 1625603005 464848 :archenoth!~archenoth@S0106889e6827f474.cg.shawcable.net JOIN :#esolangs > 1625603336 23007 PRIVMSG #esolangs :14[[07User:Dtuser1337/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=85811&oldid=85810 5* 03Dtuser1337 5* (+336) 10/* 99 Bottles of Beer */ < 1625604355 844696 :riv!~river@tilde.team/user/river PRIVMSG #esolangs :https://medium.com/@benjamin.botto/implementing-an-optimal-rubiks-cube-solver-using-korf-s-algorithm-bf750b332cf9 < 1625604359 671410 :riv!~river@tilde.team/user/river PRIVMSG #esolangs :look at he use of lehmer codes < 1625604367 873378 :riv!~river@tilde.team/user/river PRIVMSG #esolangs :https://medium.com/@benjamin.botto/sequentially-indexing-permutations-a-linear-algorithm-for-computing-lexicographic-rank-a22220ffd6e3 < 1625604371 395277 :riv!~river@tilde.team/user/river PRIVMSG #esolangs :sorry for medium links > 1625604971 98166 PRIVMSG #esolangs :14[[07Language list14]]4 10 02https://esolangs.org/w/index.php?diff=85812&oldid=85775 5* 03Sebosh 5* (-14) 10 < 1625606005 291839 :hendursa1!~weechat@user/hendursaga QUIT :Remote host closed the connection < 1625606029 711637 :hendursa1!~weechat@user/hendursaga JOIN :#esolangs < 1625606194 555961 :arseniiv!~arseniiv@94.41.6.151.dynamic.ufanet.ru QUIT :Ping timeout: 240 seconds < 1625609129 984391 :Koen!~Koen@92.167.9.109.rev.sfr.net QUIT :Ping timeout: 252 seconds < 1625610268 544275 :delta23!~delta23@user/delta23 QUIT :Ping timeout: 246 seconds < 1625610305 51229 :delta23!~delta23@user/delta23 JOIN :#esolangs > 1625611620 192477 PRIVMSG #esolangs :14[[07Shove14]]4 M10 02https://esolangs.org/w/index.php?diff=85813&oldid=85791 5* 03Ais523 5* (+39) 10perhaps this is the best way to make the space-in-code-formatting show up? > 1625611717 848762 PRIVMSG #esolangs :14[[07Shove14]]4 M10 02https://esolangs.org/w/index.php?diff=85814&oldid=85813 5* 03Ais523 5* (+25) 10add a category < 1625614442 975111 :delta23!~delta23@user/delta23 QUIT :Ping timeout: 252 seconds < 1625614766 57717 :delta23!~delta23@user/delta23 JOIN :#esolangs < 1625615230 232237 :hendursa1!~weechat@user/hendursaga QUIT :Remote host closed the connection < 1625615300 788775 :hendursa1!~weechat@user/hendursaga JOIN :#esolangs < 1625615935 457600 :delta23!~delta23@user/delta23 QUIT :Quit: Leaving