00:16:53 -!- Lord_of_Life has quit (Read error: Connection reset by peer). 00:19:12 -!- Lord_of_Life has joined. 01:11:40 -!- dbohdan has quit (Quit: ZNC 1.7.2+deb3 - https://znc.in). 01:11:52 -!- dbohdan has joined. 02:10:52 did another approach but it's much slower ( https://i.imgur.com/uMvEce9.png 03:08:36 -!- aquijoule_ has joined. 03:10:52 -!- richbridger has quit (Ping timeout: 246 seconds). 03:12:36 [[Py256]] M https://esolangs.org/w/index.php?diff=85773&oldid=84554 * Makonede * (+16) 03:43:16 -!- monoxane has quit (Quit: estoy fuera). 03:43:48 -!- monoxane has joined. 03:58:57 [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=85774&oldid=85748 * BurningApparatus * (+201) /* Introductions */ 05:01:04 https://i.imgur.com/vqjmZFl.mp4 05:35:08 -!- monoxane has quit (Quit: estoy fuera). 05:35:40 -!- monoxane has joined. 06:36:55 https://i.imgur.com/7L3ELnH.mp4 07:16:17 -!- Sgeo has quit (Read error: Connection reset by peer). 08:00:51 -!- riv has quit (Quit: Leaving). 08:06:34 -!- hendursa1 has joined. 08:09:47 -!- hendursaga has quit (Ping timeout: 244 seconds). 08:21:47 -!- Lord_of_Life_ has joined. 08:22:09 -!- Lord_of_Life has quit (Ping timeout: 252 seconds). 08:24:26 -!- Lord_of_Life_ has changed nick to Lord_of_Life. 08:44:49 Hmm, is the infinite variant of Lagrange's group theory theorem equivalent to the axiom of choice? 08:46:35 [[Special:Log/newusers]] create * Flyingmadpakke * New user account 08:49:38 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. 09:09:15 "LEM (which implies AOC)"... no 09:10:52 Yeah, AOC => LEM but not the other way around, I'm pretty sure 09:15:02 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. 09:16:31 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 09:17:09 err, encoding the fact that the sets in X are non-empty 09:19:37 -!- hanif has joined. 09:20:25 https://en.wikipedia.org/wiki/Diaconescu%27s_theorem I think 09:21:08 You're entirely correct. 09:26:07 Ah, that's a bit more clever... we *can* exhibit elements of U and V there, so it's not just an encoding quirk. 09:26:35 Taneb: thanks 09:28:11 I heard about the axiom of global choice recently. What a great axiom. 09:30:20 what's next? epsilon calculus? 09:31:34 Ah, I hadn't heard of that either. 09:31:39 -!- Koen has joined. 09:32:09 This epsilon thing is slightly reminiscent of "seemingly impossible programs". 09:32:45 Where the find operator also takes a predicate and returns a value that satisfies it, if it exists, or otherwise an unspecified value. 09:32:54 And exists and forall are implemented the same way. 09:34:16 Maybe this epsilon thing works well in some sort of compactness-related context. 09:34:36 Hmm, I still don't really know what the computational content of compactness is, in that sort of context. 10:12:21 -!- arseniiv has joined. 11:09:53 -!- Koen has quit (Remote host closed the connection). 11:16:14 -!- Koen has joined. 11:30:31 -!- Koen has quit (Remote host closed the connection). 11:51:09 -!- Koen has joined. 11:55:34 -!- hanif has quit (Ping timeout: 244 seconds). 12:09:39 -!- tromp has joined. 12:43:38 -!- hanif has joined. 12:50:11 -!- velik has quit (Remote host closed the connection). 13:56:07 -!- Sgeo has joined. 13:58:01 -!- hanif has quit (Ping timeout: 244 seconds). 14:41:46 -!- arseniiv has quit (Ping timeout: 240 seconds). 14:58:36 [[Language list]] M https://esolangs.org/w/index.php?diff=85775&oldid=85749 * PythonshellDebugwindow * (+12) /* R */ RHOVL 15:00:17 [[RHOVL]] M https://esolangs.org/w/index.php?diff=85776&oldid=85760 * PythonshellDebugwindow * (+78) /* Interpreter */ Cats 15:00:52 [[RHOVL]] M https://esolangs.org/w/index.php?diff=85777&oldid=85776 * PythonshellDebugwindow * (+70) Refimpl 15:32:18 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85778&oldid=70408 * Dtuser1337 * (+1474) /* Beginning of the Sandbox line */ 15:49:47 -!- Koen has quit (Remote host closed the connection). 15:54:10 -!- riv has joined. 16:00:55 -!- delta23 has joined. 16:05:17 [[Talk:Cheese]] https://esolangs.org/w/index.php?diff=85779&oldid=85200 * Sanscicondos * (+53) /* Know Bugs As of Version [Alpha 1.3] */ 16:15:37 -!- hanif has joined. 16:16:20 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85780&oldid=85778 * Dtuser1337 * (+569) /* Commands */ 16:21:44 -!- tromp has quit (Read error: Connection reset by peer). 16:25:15 https://i.imgur.com/y3Tg3oj.png ; https://i.imgur.com/O5sSCPR.mp4 16:31:54 -!- leah2 has quit (Ping timeout: 240 seconds). 16:32:37 https://i.imgur.com/yBhtVxG.png ; https://i.imgur.com/19kdpY0.mp4 16:34:49 -!- leah2 has joined. 16:39:44 -!- hanif has quit (Ping timeout: 244 seconds). 16:52:04 -!- arseniiv has joined. 17:06:15 [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=85781&oldid=85774 * Flyingmadpakke * (+151) /* Introductions */ 17:10:13 [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=85782&oldid=85781 * Flyingmadpakke * (+81) /* Introductions */ 17:43:54 -!- hanif has joined. 18:09:24 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85783&oldid=85780 * Dtuser1337 * (+2759) /* Commands */ 18:10:01 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85784&oldid=85783 * Dtuser1337 * (+7) /* Commands */ 18:10:24 heh, while small objects like this crater go well https://i.imgur.com/pHR2Fse.png 18:10:38 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85785&oldid=85784 * Dtuser1337 * (+0) /* Commands */ 18:10:49 this one does not ( https://i.imgur.com/NfwEnKO.png 18:11:18 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85786&oldid=85785 * Dtuser1337 * (-3) /* Commands */ 18:11:47 oh 18:12:17 I imagine I could generate the image on lower resolution and then recursively go 2 times higher 18:12:32 but it's too complex compared to current state 18:17:46 [[Talk:Truth-machine]] https://esolangs.org/w/index.php?diff=85787&oldid=77361 * Flyingmadpakke * (+1507) 18:26:07 -!- Oshawott has quit (Ping timeout: 246 seconds). 18:27:47 -!- hanif has quit (Quit: quit). 18:32:14 [[\ () /]] https://esolangs.org/w/index.php?diff=85788&oldid=81658 * LegionMammal978 * (+226) fix links 18:53:53 [[DROL]] https://esolangs.org/w/index.php?diff=85789&oldid=81673 * LegionMammal978 * (+10) /* External Links */ fix links 18:58:44 I guess I'll stop on this for now 19:02:42 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85790&oldid=85786 * Dtuser1337 * (+1826) /* Commands */ 19:12:21 [[Shove]] M https://esolangs.org/w/index.php?diff=85791&oldid=44005 * OrichalcumCosmonaut * (-13) fix spacing of and un-preformat the space instruction 19:19:18 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85792&oldid=85790 * Dtuser1337 * (+958) /* Commands */ 19:25:03 [[Muddle]] https://esolangs.org/w/index.php?diff=85793&oldid=77988 * LegionMammal978 * (+8) /* Interpreter */ fix links 19:27:38 is the singingbanana on the esowiki the same singingbanana that does the numberphile videos? 19:30:29 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85794&oldid=85792 * Dtuser1337 * (+150) 19:35:56 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85795&oldid=85794 * Dtuser1337 * (+108) 19:38:28 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85796&oldid=85795 * Dtuser1337 * (+100) /* Commands */ 19:41:59 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85797&oldid=85796 * Dtuser1337 * (-79) /* Beginning of the Sandbox line */ 19:43:28 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85798&oldid=85797 * Dtuser1337 * (+40) /* Beginning of the Sandbox line */ 19:44:34 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85799&oldid=85798 * Dtuser1337 * (-12) /* Commands */ 19:46:07 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85800&oldid=85799 * Dtuser1337 * (+7) /* Commands */ 19:49:56 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85801&oldid=85800 * Dtuser1337 * (+50) /* Examples */ 20:05:50 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85802&oldid=85801 * Dtuser1337 * (+375) /* Examples */ 20:12:29 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85803&oldid=85802 * Dtuser1337 * (+235) /* Function Commands */ 20:12:45 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85804&oldid=85803 * Dtuser1337 * (-1) /* Function Commands */ 20:15:11 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85805&oldid=85804 * Dtuser1337 * (+32) /* Function Commands */ 20:15:45 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85806&oldid=85805 * Dtuser1337 * (-13) /* Function Commands */ 20:16:54 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85807&oldid=85806 * Dtuser1337 * (-11) /* Cat */ 20:17:45 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85808&oldid=85807 * Dtuser1337 * (+30) /* File I/O Commands */ 20:18:12 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85809&oldid=85808 * Dtuser1337 * (+0) /* File I/O Commands */ 20:18:33 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85810&oldid=85809 * Dtuser1337 * (+13) /* File I/O Commands */ 20:22:07 -!- Koen has joined. 20:23:25 -!- archenoth has joined. 20:28:56 [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85811&oldid=85810 * Dtuser1337 * (+336) /* 99 Bottles of Beer */ 20:45:55 https://medium.com/@benjamin.botto/implementing-an-optimal-rubiks-cube-solver-using-korf-s-algorithm-bf750b332cf9 20:45:59 look at he use of lehmer codes 20:46:07 https://medium.com/@benjamin.botto/sequentially-indexing-permutations-a-linear-algorithm-for-computing-lexicographic-rank-a22220ffd6e3 20:46:11 sorry for medium links 20:56:11 [[Language list]] https://esolangs.org/w/index.php?diff=85812&oldid=85775 * Sebosh * (-14) 21:13:25 -!- hendursa1 has quit (Remote host closed the connection). 21:13:49 -!- hendursa1 has joined. 21:16:34 -!- arseniiv has quit (Ping timeout: 240 seconds). 22:05:29 -!- Koen has quit (Ping timeout: 252 seconds). 22:24:28 -!- delta23 has quit (Ping timeout: 246 seconds). 22:25:05 -!- delta23 has joined. 22:47:00 [[Shove]] M https://esolangs.org/w/index.php?diff=85813&oldid=85791 * Ais523 * (+39) perhaps this is the best way to make the space-in-code-formatting show up? 22:48:37 [[Shove]] M https://esolangs.org/w/index.php?diff=85814&oldid=85813 * Ais523 * (+25) add a category 23:34:02 -!- delta23 has quit (Ping timeout: 252 seconds). 23:39:26 -!- delta23 has joined. 23:47:10 -!- hendursa1 has quit (Remote host closed the connection). 23:48:20 -!- hendursa1 has joined. 23:58:55 -!- delta23 has quit (Quit: Leaving).