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 <nakilon> 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 <esolangs> [[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 <esolangs> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=85774&oldid=85748 * BurningApparatus * (+201) /* Introductions */
05:01:04 <nakilon> https://i.imgur.com/vqjmZFl.mp4
05:35:08 -!- monoxane has quit (Quit: estoy fuera).
05:35:40 -!- monoxane has joined.
06:36:55 <nakilon> 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 <Taneb> Hmm, is the infinite variant of Lagrange's group theory theorem equivalent to the axiom of choice?
08:46:35 <esolangs> [[Special:Log/newusers]] create * Flyingmadpakke * New user account
08:49:38 <Corbin> 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 <int-e> "LEM (which implies AOC)"... no
09:10:52 <Taneb> Yeah, AOC => LEM but not the other way around, I'm pretty sure
09:15:02 <int-e> 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 <int-e> 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 <int-e> err, encoding the fact that the sets in X are non-empty
09:19:37 -!- hanif has joined.
09:20:25 <Taneb> https://en.wikipedia.org/wiki/Diaconescu%27s_theorem I think
09:21:08 <Corbin> You're entirely correct.
09:26:07 <int-e> 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:28:11 <shachaf> I heard about the axiom of global choice recently. What a great axiom.
09:30:20 <int-e> what's next? epsilon calculus?
09:31:34 <shachaf> Ah, I hadn't heard of that either.
09:31:39 -!- Koen has joined.
09:32:09 <shachaf> This epsilon thing is slightly reminiscent of "seemingly impossible programs".
09:32:45 <shachaf> 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 <shachaf> And exists and forall are implemented the same way.
09:34:16 <shachaf> Maybe this epsilon thing works well in some sort of compactness-related context.
09:34:36 <shachaf> 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 <esolangs> [[Language list]] M https://esolangs.org/w/index.php?diff=85775&oldid=85749 * PythonshellDebugwindow * (+12) /* R */ RHOVL
15:00:17 <esolangs> [[RHOVL]] M https://esolangs.org/w/index.php?diff=85776&oldid=85760 * PythonshellDebugwindow * (+78) /* Interpreter */ Cats
15:00:52 <esolangs> [[RHOVL]] M https://esolangs.org/w/index.php?diff=85777&oldid=85776 * PythonshellDebugwindow * (+70) Refimpl
15:32:18 <esolangs> [[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 <esolangs> [[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 <esolangs> [[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 <nakilon> 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 <nakilon> 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 <esolangs> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=85781&oldid=85774 * Flyingmadpakke * (+151) /* Introductions */
17:10:13 <esolangs> [[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 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85783&oldid=85780 * Dtuser1337 * (+2759) /* Commands */
18:10:01 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85784&oldid=85783 * Dtuser1337 * (+7) /* Commands */
18:10:24 <nakilon> heh, while small objects like this crater go well https://i.imgur.com/pHR2Fse.png
18:10:38 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85785&oldid=85784 * Dtuser1337 * (+0) /* Commands */
18:10:49 <nakilon> this one does not ( https://i.imgur.com/NfwEnKO.png
18:11:18 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85786&oldid=85785 * Dtuser1337 * (-3) /* Commands */
18:12:17 <nakilon> I imagine I could generate the image on lower resolution and then recursively go 2 times higher
18:12:32 <nakilon> but it's too complex compared to current state
18:17:46 <esolangs> [[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 <esolangs> [[\ () /]] https://esolangs.org/w/index.php?diff=85788&oldid=81658 * LegionMammal978 * (+226) fix links
18:53:53 <esolangs> [[DROL]] https://esolangs.org/w/index.php?diff=85789&oldid=81673 * LegionMammal978 * (+10) /* External Links */ fix links
18:58:44 <nakilon> I guess I'll stop on this for now
19:02:42 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85790&oldid=85786 * Dtuser1337 * (+1826) /* Commands */
19:12:21 <esolangs> [[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 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85792&oldid=85790 * Dtuser1337 * (+958) /* Commands */
19:25:03 <esolangs> [[Muddle]] https://esolangs.org/w/index.php?diff=85793&oldid=77988 * LegionMammal978 * (+8) /* Interpreter */ fix links
19:27:38 <imode> is the singingbanana on the esowiki the same singingbanana that does the numberphile videos?
19:30:29 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85794&oldid=85792 * Dtuser1337 * (+150)
19:35:56 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85795&oldid=85794 * Dtuser1337 * (+108)
19:38:28 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85796&oldid=85795 * Dtuser1337 * (+100) /* Commands */
19:41:59 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85797&oldid=85796 * Dtuser1337 * (-79) /* Beginning of the Sandbox line */
19:43:28 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85798&oldid=85797 * Dtuser1337 * (+40) /* Beginning of the Sandbox line */
19:44:34 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85799&oldid=85798 * Dtuser1337 * (-12) /* Commands */
19:46:07 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85800&oldid=85799 * Dtuser1337 * (+7) /* Commands */
19:49:56 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85801&oldid=85800 * Dtuser1337 * (+50) /* Examples */
20:05:50 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85802&oldid=85801 * Dtuser1337 * (+375) /* Examples */
20:12:29 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85803&oldid=85802 * Dtuser1337 * (+235) /* Function Commands */
20:12:45 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85804&oldid=85803 * Dtuser1337 * (-1) /* Function Commands */
20:15:11 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85805&oldid=85804 * Dtuser1337 * (+32) /* Function Commands */
20:15:45 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85806&oldid=85805 * Dtuser1337 * (-13) /* Function Commands */
20:16:54 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85807&oldid=85806 * Dtuser1337 * (-11) /* Cat */
20:17:45 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85808&oldid=85807 * Dtuser1337 * (+30) /* File I/O Commands */
20:18:12 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85809&oldid=85808 * Dtuser1337 * (+0) /* File I/O Commands */
20:18:33 <esolangs> [[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 <esolangs> [[User:Dtuser1337/Sandbox]] https://esolangs.org/w/index.php?diff=85811&oldid=85810 * Dtuser1337 * (+336) /* 99 Bottles of Beer */
20:45:55 <riv> https://medium.com/@benjamin.botto/implementing-an-optimal-rubiks-cube-solver-using-korf-s-algorithm-bf750b332cf9
20:45:59 <riv> look at he use of lehmer codes
20:46:07 <riv> https://medium.com/@benjamin.botto/sequentially-indexing-permutations-a-linear-algorithm-for-computing-lexicographic-rank-a22220ffd6e3
20:46:11 <riv> sorry for medium links
20:56:11 <esolangs> [[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 <esolangs> [[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 <esolangs> [[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).