> 1769213478 386839 PRIVMSG #esolangs :14[[07Talk:Combinatory logic14]]4 10 02https://esolangs.org/w/index.php?diff=174151&oldid=174150 5* 03Corbin 5* (+192) 10/* Is there anything between IJ and complete bases? */ Good question. > 1769217084 908953 PRIVMSG #esolangs :14[[07Execline14]]4 10 02https://esolangs.org/w/index.php?diff=174152&oldid=147774 5* 03Corbin 5* (+542) 10Style, references, bluelinks, more words. > 1769217912 468752 PRIVMSG #esolangs :14[[07Vixen14]]4 10 02https://esolangs.org/w/index.php?diff=174153&oldid=170776 5* 03Corbin 5* (+775) 10Senpai noticed me! Save a couple quotes which I think are, in sequence, *extremely* funny. Also explain the name more. < 1769217934 913122 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :It's Foxgirl Friday, after all. < 1769217967 620734 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :https://media.bark.lgbt/media_attachments/files/112/019/720/787/034/539/original/40a24e0f8465b9ca.jpg < 1769218226 104472 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I am still bothered at the overly literal romanisation "senpai" – romanizations of Japanese are mostly intended to allow English speakers to read and pronounce the word more easily, so it should probably be spelled "sempai" which is also valid and much closer to the actual Japanese pronunciation < 1769218333 763885 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :"senpai" would work well if it were being used to type Japanese on an English keyboard, but I don't think that's the usual motivation < 1769218372 55113 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Uguu~ I'm just surrounded by senpai~ < 1769218394 199537 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :As usual, I am half-serious and half-joking, right down the middle like a chimeric housecat. < 1769218486 852785 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I guess Japanese loanwords from English have often diverged quite some way from their initial English pronunciations and even meanings, so the same happening in reverse isn't so surprising < 1769218527 746705 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Anyway, I guess Vixen is officially a Linux spin. I have successfully called Vixen methods from inside QEMU after using a Vixen method as the /init. I am tempted to ask for [[Category:Linux distributions]]. < 1769218615 645397 :Sgeo!~Sgeo@user/sgeo PRIVMSG #esolangs :I vaguely started reading about Lean and Rocq, there's an interactive "game" for learning Lean. < 1769218638 716989 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :We kind of have a PNW Japanese dialect and accent. Second-gen folks have an l/r split, and the gendered words are heavily disfavored. There's still a fairly strong distinction between the native speakers and the folks like me who have it as third or fourth language. < 1769218655 573517 :Sgeo!~Sgeo@user/sgeo PRIVMSG #esolangs :Can those proof things use intuitionistic logic? Or only their own builtin one? I kind of think intuitionistic logic is a bit... unintuitive < 1769218751 4686 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Sgeo: They aren't really designed for implementing logic in logic. It's a longstanding issue with the type-theory approach to proofs. I don't know what Lean's formalism actually is today ("unsound" TBH) but Rocq's using a fairly nice higher-order lambda calculus, Calculus of Constructions. < 1769218808 289318 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Contrast with e.g. Metamath where there's set.mm using classical logic and ZFC next to iset.mm using intuitionistic logic and IZF. And further down the road they also have quantum foundations. I tried to contribute linear-logic foundations a few years ago, based on a paper of M. Shulman, but couldn't get it to actually work. < 1769218890 857423 :Sgeo!~Sgeo@user/sgeo PRIVMSG #esolangs :Would learning about Metamath be a good way to learn... about ZFC and ... other stuff? < 1769218961 873916 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :To answer your earlier question, here's how to make Rocq do any logic you want; the example's fully worked to prove Gödel's theorem, but it could be adjusted to write an interpreter or etc. https://www.r6.ca/Goedel/goedel1.html < 1769219028 241978 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :TBH maybe but probably not. Metamath can help with understanding practical foundations of logic, but it's not a teaching tool. Metamath's real power is that it verifies thousands of proofs/second. What set.mm can teach you is how to start with complex numbers before natural numbers. < 1769219060 769433 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I get frustrated that Rust doesn't appear to be implemented by desugaring everything into a smaller core language, which has lead to a number of soundness bugs < 1769219137 619925 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Sgeo: Ah, found it. If you want to understand the *structural ideas* underneath ZFC, I really recommend https://arxiv.org/abs/1212.6543 by Leinster. ZFC itself is a specific programming language where the only datatype is sets. It's verbose and nasty. Leinster cleans it all up. < 1769219139 496117 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :(a good example is my answer https://stackoverflow.com/q/79825066 which got it into the Hot Network Questions sidebar, something that is more to do on Stack Overflow than on smaller Stack Exchange sites, although the "this is caused by not implementing as desugaring" is explained only in the comments) < 1769219145 875521 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :* my answer to < 1769219222 564241 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523: Nice answer. For some reason I can't articulate yet, this feels like the same shape as finalizers in GC'd runtimes. < 1769219245 223974 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I guess it's the illegal-looking self-extension of a finalizer's effective lifetime via ordinary mutation. < 1769219279 863820 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I think I tried to seriously use resurrection-within-finalizer as part of a serious Java project once, but can no longer remember the details < 1769219292 425796 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I do remember that it either didn't work or was unnecessary, possibly both < 1769219309 932525 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I may have used it in a Minecraft server? I'll check. < 1769219486 695263 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Oh wow. Nope, instead I apparently *never deleted* the relevant objects. Hilarious code from Past Corbin there. < 1769219519 815724 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :intentional memory leaks are an underrated coding technique < 1769220116 232147 :amby!~ambylastn@host-81-178-158-197.as13285.net QUIT :Remote host closed the connection < 1769220564 961363 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :ais523: what kind of smaller core language are you thinking of? normally I'd think of one that helps compiling to various CPU native codes, but you have to verify that the program typechecks and lifetime checks before you compile to the small core language, because the core language doesn't ensure safety anymore. but I thought most soundness bugs in rust are from confusing the typechecker. < 1769220594 76789 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :b_jonas: a type system based on fewer primitives < 1769220624 139848 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :as an example, currently in Rust a closure is its own thing that acts sort-of like a struct – I would prefer it if closures were just desugared directly to structs, and then typechecked in that form < 1769220655 429857 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :hmm > 1769220721 69357 PRIVMSG #esolangs :14[[07User talk:RetroPain14]]4 M10 02https://esolangs.org/w/index.php?diff=174154&oldid=174013 5* 03RetroPain 5* (+5) 10 < 1769220724 400129 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :well-formedness is another good example, instead of being a rule of the type system the compiler could just desugar into stating the well-formedness-implied bounds explicitly and then check those > 1769220734 790900 PRIVMSG #esolangs :14[[07User talk:RetroPain14]]4 M10 02https://esolangs.org/w/index.php?diff=174155&oldid=174154 5* 03RetroPain 5* (-5) 10test < 1769220739 570776 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :translating closures to structs is probably possible to simplify compilation, though I don't know if it's also possible in a way that it's enough to do typechecking after the transformation < 1769220762 111288 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :what do you mean by well-formedness? > 1769220763 318946 PRIVMSG #esolangs :14[[07User talk:RetroPain14]]4 10 02https://esolangs.org/w/index.php?diff=174156&oldid=174155 5* 03RetroPain 5* (+100) 10 < 1769220781 732734 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :do you mean no type names with loops? < 1769220824 904555 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :b_jonas: a &'a T can't exist if T contains a lifetime shorter than 'a < 1769220839 156145 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :like, it can't even be mentioned by the type system or it causes horrible type system bugs < 1769220878 135864 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :this sort-of makes sense because a &'a T is supposed to always contain a valid T for the entire lifetime 'a, which it couldn't if T becomes invalid at some point during 'a < 1769220904 52313 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but it seems wrong to me that it breaks on even mentioning the type, even if objects of that type are never constructed < 1769220910 411502 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :I See < 1769220987 231717 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :I think part of the reason why rustc doesn't try to desugar constructs to a simpler language is that rustc tries to give very readable error/warning messages, more so than gcc/clang, and desugaring would make that harder because you'd have to resugar to print the error/warning < 1769221095 161145 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :I mean the error/warning messages not only try to prove that your code is wrong, they also often try to give a guess of what you may have meant to write < 1769221097 753922 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Same philosophy as GHC, right? < 1769221097 956174 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :that is plausible, I was wondering about it myself < 1769221123 283284 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but you don't really need to resugar, just look at the corresponding initial code < 1769221179 221033 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :yes, but you need to analyze the initial code to guess what the user meant to write < 1769221288 661500 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :anyway, maybe some translation could be done, I was just confused because when you say "translate to a smaller language" I mostly think of one that no longer knows about lifetimes and only implements unsafe rust, and even loses some of the type information besides lifetimes so it can do type-unsafe things < 1769221354 152622 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :b_jonas: Rust already does that step internally < 1769221358 331223 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :but closures in particular you can probably translate away, also you can probably eliminate the complex pattern language and let-chains and only use simple match statements on the top-level enum constructor < 1769221362 383691 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :so I can't reasonably criticise it for not doing that < 1769221715 643859 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :I still don't know whether you can actually translate rust to a language that has conditional gotos instead of loops. I hope it can be. < 1769222707 428773 :impomatic!~impomatic@2a00:23c7:5fc6:3201:d844:8367:241f:5119 QUIT :Quit: Client closed < 1769225880 378915 :Hooloovoo!~Hooloovoo@hax0rbana.org PRIVMSG #esolangs :doesn't it compile to assembly? < 1769226061 199829 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :Hooloovoo: yes, but this is about intermediate forms before that > 1769226149 775782 PRIVMSG #esolangs :14[[07Endfield14]]4 N10 02https://esolangs.org/w/index.php?oldid=174157 5* 03Cleverxia 5* (+1800) 10Created page with "Endfield is yet another esolang created by [[User:cleverxia]]. It's a brainfuck derivative. The commands are due to the fact that when you pay to the game Endfield, it deduces money from a random account, and you can login on your account on other devices wit cache < 1769226196 477068 :Hooloovoo!~Hooloovoo@hax0rbana.org PRIVMSG #esolangs :I will admit that the last question was basically the only part of the conversation I understood fully > 1769226197 933820 PRIVMSG #esolangs :14[[07User:Cleverxia14]]4 10 02https://esolangs.org/w/index.php?diff=174158&oldid=174087 5* 03Cleverxia 5* (+43) 10/* Current Esolangs I've created */ < 1769233424 153714 :Sgeo!~Sgeo@user/sgeo PRIVMSG #esolangs :I don't understand true but not provable. Is the continuum hypothesis a statement that might be true but not provable? I'm vaguely under the impression that there's a way to envision ZFC where CH is true and a way to envision it where it's false. So is that... a different sort of thing from statements which might be true but not provably true? < 1769234068 245906 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Kind of. CH is *independent*. Like, suppose we have a function f(0) = N, f(n + 1) = f(n) → 2. This is the iterated power set of the natural numbers. (This could be called aleph or bet in some texts, but it's not consistent.) < 1769234157 467815 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :CH says that f(1) = R. Cantor's theorem says N ≠ R, so f(0) ≠ R. But other than that, it turns out that we can construct worlds where f(k) = R for any nonzero k, your choice, made to order. So CH is independent of the usual rules of set theory; it's a free choice to make. < 1769234242 644216 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Gödel's true-but-unprovable is something different. There's a standard answer and a non-standard answer. Let G be true-but-unprovable; you the human are convinced G is true by construction, but that same construction says ZFC cannot prove G. < 1769234294 953916 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :The standard answer is that G is true, so ZFC + G is a fine theory. Indeed the model of natural numbers we get this way is the same one as before; we have this new true fact G which doesn't contradict ZFC's axioms at all and which we couldn't reach otherwise. < 1769234297 161650 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :CH is provably (in PRA or weaker systems) not provable or disprovable in ZFC. Whether CH is true, false, or objectively meaningless is a philosophical question outside the scope of formal mathematics < 1769234379 551279 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :We can also try ZFC + ~G but it's non-standard, which is how we say "weird" in model theory. ~G means that there *is* a proof of G, somewhere out there in the ether. By tradition, call its Gödel number c. c isn't a finite natural number, but more like a constant for a polynomial ring. < 1769234415 224763 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :(in every set theory text I've seen, beth = iterated power set of the naturals, aleph = iterated cardinal successor of the naturals, beth(1) = R, CH is "aleph(1) also = R") < 1769234498 375771 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :the cardinal successor of a set S is a bit abstract but can be interpreted as the number of order types of at most S elements, so aleph(1) is the set of countable ordinals < 1769234573 863566 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Sgeo: Sorry if that's kind of an infodump. In short, let CH(k) := f(k) = R, then ZFC + CH(1) and ZFC + CH(2) and ZFC + CH(k) in general and also ZFC + G are good theories that do what you expect, and ZFC + ~G has a non-standard model. < 1769234686 930361 :Sgeo!~Sgeo@user/sgeo PRIVMSG #esolangs :I tried to wrap my mind around non-standard models, and got so far as to understand that stuff like "a number other than the natural numbers that fits within the Peano axioms" is an example but not the only one < 1769234742 611458 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :sorear: Interestingly, it comes up in category theory, but not for the normal size-issue reasons; it turns out that "all beths exist" is independent of structural set theory. Category theory just doesn't have the big cardinals by default. TBH our foundations can't even distinguish ordinals and cardinals! < 1769234861 451033 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Sgeo: There's a kind of semiotic/graph approach, and there's also a game-semantics approach. And yeah, I can give another example really easily once we understand either approach for a Gödel model. < 1769234932 662450 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :If you have a model of ZFC you can construct a model of ZFC + CH (e.g. Godel's L) and a model of ZFC + ~CH (e.g. omega(2) Cohen reals). You can recast both of these as interpretations and avoid the problems associated with a model < 1769234951 84151 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :In terms of graphs, we can structure the natural numbers as 0 → 1 → 2 → …, one long chain with one starting point. An object is a model of nats precisely when we can find this chain structure somewhere inside it. < 1769235031 491498 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :The successor axiom says that progressing along this chain is a function. But that's really the only hard rule. So a Gödel model just imagines that there's another chain, … → c -1 → c → c + 1 → … floating along, inaccessible from the initial chain. < 1769235094 757688 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :you usually want the Rosser sentence instead "for every proof of this statement there is a shorter proof of its negation" < 1769235126 411955 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :We can also drop the requirement that successors are injective. So in that case we could have models that start at some side constant c → c + 1 → … → 1 → 2 → … And those are non-standard as well. A model just has to have that initial chain, or "initial segment" in the literature. < 1769235314 951242 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Sgeo: I guess another important thing is that non-standard models *of arithmetic* and *of set theory* are distinct. I kind of assumed that you were looking at the former, since Gödel, but the latter are relevant to history of CH. Sorry for being confusing if that's the case. < 1769235359 705546 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :there are no computable models of PA + ~G, most of interest that you can say about them starts from Henkin's theorem (all consistent first-order theories have models) < 1769235409 218473 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :this is non-constructive since it involves infinitely iteration of the law of the excluded middle, but definable in the set-theoretic sense since you didn't touch choice < 1769235592 120267 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :"non-standard model of set theory" is not particularly standard terminology. both L and forcing models have externally well-ordered ordinals and satisfy exactly the same arithmetical statements as the metatheory < 1769235610 882936 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :IIRC there's no computable models of PA besides the standard model; this is called "Tenenbaum's theorem" or something like that. < 1769235793 844650 :Sgeo!~Sgeo@user/sgeo PRIVMSG #esolangs :What does this mean for BB(745), which is apparently... independent of ZFC? It feels like that value should, in some platonic sense, have a single correct value < 1769235829 429122 :Sgeo!~Sgeo@user/sgeo PRIVMSG #esolangs :Unless there's a non-standard ZFC where turing machines behave weirdly < 1769235898 561262 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :unless you're an ultrafinitist that TM either halts after some finite number of steps or it doesn't, sigma_1 arithmetical sentence < 1769235899 638453 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :It means that there's no valid proof in ZFC that decodes at a high level to `BB(745) = k` for any natural k. For if there were, then we have a program that would search for it s.t. we can derive a contradiction from ZFC's axioms. < 1769235991 614406 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :BB is a well-defined function N → N, ZFC just turns out to be too weak of a theory~ < 1769236022 527475 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :finished a proof in HOL last year that there is a turing machine T with 748 states such that T halts iff ZFC is inconsistent < 1769236050 478301 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I guess that we can connect this to true-but-unprovable. BB is total-but-uncomputable relative to ZFC, also relative to SRP or basically any other large-cardinal theory. > 1769236088 990716 PRIVMSG #esolangs :14[[07User:None1/InDev14]]4 10 02https://esolangs.org/w/index.php?diff=174159&oldid=174131 5* 03None1 5* (+123) 10/* Commands */ < 1769236168 472527 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Sgeo: Oh! If you've seen Gödel's Second Incompleteness, then this is a way to think of that result. Gödel says that no finite collection of axioms can capture all the true statements of arithmetic. The BB function happens to give us a metric for measuring how far a set of axioms goes before it runs out of proof power. > 1769236263 1481 PRIVMSG #esolangs :14[[07User:None1/InDev14]]4 10 02https://esolangs.org/w/index.php?diff=174160&oldid=174159 5* 03None1 5* (+139) 10/* Commands */ < 1769236286 32906 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :if T halts in less than k steps, then ZFC is inconsistent with a concrete example. if T does not halt in less than k steps (a delta_0 statement, and provable if true in all systems stronger than Q) and BB(748) = k, then (in ZFC) T does not halt and therefore ZFC proves its own consistency and is inconsistent per Godel < 1769236965 178185 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :sorear: Oh wow, that just clicked for me. Nice! Was that in Lean, Isabelle, or something else? < 1769237018 455507 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :hol-light, we discussed it a little bit < 1769237084 468678 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Oh yeah. And it's in my notes. I just forgot. < 1769237102 147532 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ACTION ditzy < 1769237203 596208 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :korvo: I think your statement of the continuum hypothesis is wrong – N→2 is known to have the same cardinality as the reals (this is pretty easy to prove), the question is as to whether there's anything with a cardinality between that of N and R < 1769237314 864023 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523: That sounds entirely reasonable. I have yet to actually look anything up and I do often emit plausible-sounding bullshit. < 1769237560 603951 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :hmm, an interesting way to view the busy beaver function is as a map from the size of a false conjecture to the size of the smallest counterexample to it < 1769237641 256901 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :so knowing the values of the busy beaver function would let you prove anything by brute-forcing for counterexamples – but the only way to actually calculate the values in the first place is to check every possible conjecture of a given size and try to prove or disprove it, so trying to use the function for that purpose doesn't help < 1769237807 536587 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :and now I'm thinking about the fact that any prefix of the busy beaver function is theoretically computable just by hardcoding the values, but no program can encode the entire sequence because it will eventually discover a conjecture about its own behaviour < 1769237813 735939 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :chaitin's constant might be more useful in that direction < 1769237838 384631 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :well, they're both similarly useful, it's just that for Chaitin's constant the brute-forcing is faster < 1769237894 377012 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :or, hmm, is it even faster? thinking about it, it's probably slower, because you have to run all the other programs too in order to see which ones halt earlier < 1769237971 424565 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :(although Chaitin's constant does have the advantage of working with reasonable-sized numbers rather than Busy Beaver-sized numbers, I don't think that advantage actually helps once you start actually doing the brute-forcing) < 1769238238 551483 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :oh yeah, korvo's first formulation was indeed wrong, I didn't even notice < 1769238280 562242 :b_jonas!~x@catv-80-98-84-202.catv.fixed.one.hu PRIVMSG #esolangs :but I think sorear gave the correct one later < 1769238315 484028 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :My purpose in life is to be wrong, misleading, or straight-up incorrect. < 1769238385 587321 :int-e!~noone@int-e.eu PRIVMSG #esolangs :born to be llm < 1769238420 290633 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :if the universe turns out not to be discretizable in meaningful way we can ask if CH corresponds to a meaningful physical question, even if formal mathematics has little to say about it < 1769240402 688645 :ais523!~ais523@user/ais523 QUIT :Quit: quit > 1769240584 613099 PRIVMSG #esolangs :14[[07Talk:Polynomix14]]4 10 02https://esolangs.org/w/index.php?diff=174161&oldid=173962 5* 03Yayimhere2(school) 5* (-2) 10/* user:Yayimhere's suggestions */ > 1769242268 783544 PRIVMSG #esolangs :14[[07Talk:Combinatory logic14]]4 10 02https://esolangs.org/w/index.php?diff=174162&oldid=174151 5* 03Blashyrkh 5* (+344) 10/* Is there anything between IJ and complete bases? */ Preliminary simulation results > 1769243325 404830 PRIVMSG #esolangs :14[[07Cammy14]]4 10 02https://esolangs.org/w/index.php?diff=174163&oldid=172438 5* 03Yayimhere2(school) 5* (+12) 10Change just "corbin" to "Corbin Simpson", and link to the relevant page, in the infobox. > 1769243422 207456 PRIVMSG #esolangs :14[[07Lye14]]4 10 02https://esolangs.org/w/index.php?diff=174164&oldid=170193 5* 03Yayimhere2(school) 5* (+3) 10[[User:Corbin]] -> Corbin Simpson, and link to relevant page(infobox) > 1769243462 213565 PRIVMSG #esolangs :14[[07Monte14]]4 10 02https://esolangs.org/w/index.php?diff=174165&oldid=166467 5* 03Yayimhere2(school) 5* (+3) 10[[User:Corbin]] -> Corbin Simpson, link to relevant page in infobox. > 1769243514 817497 PRIVMSG #esolangs :14[[07Zaddy14]]4 10 02https://esolangs.org/w/index.php?diff=174166&oldid=161275 5* 03Yayimhere2(school) 5* (+12) 10User:Corbin -> Corbin Simpson, and link to relevant page in infobox. > 1769244646 441419 PRIVMSG #esolangs :14[[07User:Blashyrkh14]]4 10 02https://esolangs.org/w/index.php?diff=174167&oldid=172687 5* 03Blashyrkh 5* (+149) 10 > 1769245280 388928 PRIVMSG #esolangs :14[[07User:Blashyrkh/Between IJ and SK14]]4 N10 02https://esolangs.org/w/index.php?oldid=174168 5* 03Blashyrkh 5* (+1460) 10Created page with "Is there a non-complete system of combinators that includes IJ system as a subset? Equivalent: is there a cancellative combinator X for which K combinator can't be expressed in IJX basis? The opposite question: is it enough to add ''any'' can < 1769245780 208712 :Sgeo!~Sgeo@user/sgeo QUIT :Read error: Connection reset by peer > 1769246048 96712 PRIVMSG #esolangs :14[[07User talk:Blashyrkh/Between IJ and SK14]]4 N10 02https://esolangs.org/w/index.php?oldid=174169 5* 03Yayimhere2(school) 5* (+141) 10Created page with "Can we get the program? --~~~~" > 1769246811 656593 PRIVMSG #esolangs :14[[07Talk:Vixen14]]4 N10 02https://esolangs.org/w/index.php?oldid=174170 5* 03Yayimhere2(school) 5* (+133) 10Created page with "exTREMELY cool. --~~~~" > 1769246973 979322 PRIVMSG #esolangs :14[[07User:Yayimhere14]]4 10 02https://esolangs.org/w/index.php?diff=174171&oldid=174008 5* 03Yayimhere2(school) 5* (+81) 10 > 1769247023 737107 PRIVMSG #esolangs :14[[07User:Yayimhere14]]4 10 02https://esolangs.org/w/index.php?diff=174172&oldid=174171 5* 03Yayimhere2(school) 5* (-1) 10 > 1769247051 426569 PRIVMSG #esolangs :14[[07User talk:Blashyrkh/Between IJ and SK14]]4 10 02https://esolangs.org/w/index.php?diff=174173&oldid=174169 5* 03Blashyrkh 5* (+390) 10 < 1769247378 339811 :Yayimhere!~Yayimhere@197.185.190.142 JOIN #esolangs * :[https://web.libera.chat] Yayimhere < 1769247384 57594 :Yayimhere!~Yayimhere@197.185.190.142 PRIVMSG #esolangs :hello! > 1769247470 364501 PRIVMSG #esolangs :14[[07Anti-Plushie language DIY14]]4 10 02https://esolangs.org/w/index.php?diff=174174&oldid=169071 5* 03PrySigneToFry 5* (+79) 10 > 1769247573 62899 PRIVMSG #esolangs :14[[07Anti-Plushie language14]]4 10 02https://esolangs.org/w/index.php?diff=174175&oldid=169075 5* 03Yayimhere2(school) 5* (+37) 10/* Commands */ > 1769247606 464467 PRIVMSG #esolangs :14[[07Talk:Anti-Plushie language DIY14]]4 10 02https://esolangs.org/w/index.php?diff=174176&oldid=173964 5* 03Yayimhere2(school) 5* (+141) 10 > 1769248324 540310 PRIVMSG #esolangs :14[[07InterpretMe14]]4 10 02https://esolangs.org/w/index.php?diff=174177&oldid=155389 5* 03Yayimhere2(school) 5* (+29) 10/* Lua */ make a see also section, with [[serious]] linked. > 1769248333 32022 PRIVMSG #esolangs :14[[07InterpretMe14]]4 10 02https://esolangs.org/w/index.php?diff=174178&oldid=174177 5* 03Yayimhere2(school) 5* (+4) 10/* See also */ > 1769248353 359571 PRIVMSG #esolangs :14[[07Serious14]]4 10 02https://esolangs.org/w/index.php?diff=174179&oldid=172629 5* 03Yayimhere2(school) 5* (+30) 10 > 1769248530 648243 PRIVMSG #esolangs :14[[07Serious14]]4 10 02https://esolangs.org/w/index.php?diff=174180&oldid=174179 5* 03Yayimhere2(school) 5* (+129) 10 < 1769248558 255246 :Yayimhere!~Yayimhere@197.185.190.142 QUIT :Quit: Client closed > 1769249379 714590 PRIVMSG #esolangs :14[[07User:Blashyrkh/Between IJ and SK14]]4 10 02https://esolangs.org/w/index.php?diff=174181&oldid=174168 5* 03Blashyrkh 5* (+61) 10Link to the program > 1769249464 991545 PRIVMSG #esolangs :14[[07User:Blashyrkh/Between IJ and SK14]]4 M10 02https://esolangs.org/w/index.php?diff=174182&oldid=174181 5* 03Blashyrkh 5* (+85) 10More search results > 1769249736 517809 PRIVMSG #esolangs :14[[07User talk:Blashyrkh/Between IJ and SK14]]4 M10 02https://esolangs.org/w/index.php?diff=174183&oldid=174173 5* 03Blashyrkh 5* (+198) 10how to build and run > 1769251073 433736 PRIVMSG #esolangs :14[[07User:Blashyrkh/Between IJ and SK14]]4 10 02https://esolangs.org/w/index.php?diff=174184&oldid=174182 5* 03Blashyrkh 5* (+722) 10more (and no more) search results > 1769251298 978622 PRIVMSG #esolangs :14[[07User:Blashyrkh/Between IJ and SK14]]4 M10 02https://esolangs.org/w/index.php?diff=174185&oldid=174184 5* 03Blashyrkh 5* (-4) 10reword > 1769251488 244889 PRIVMSG #esolangs :14[[07Talk:Combinatory logic14]]4 M10 02https://esolangs.org/w/index.php?diff=174186&oldid=174162 5* 03Blashyrkh 5* (+49) 10/* Is there anything between IJ and complete bases? */ link to the page with search results > 1769252000 241969 PRIVMSG #esolangs :14[[07Mezzo14]]4 10 02https://esolangs.org/w/index.php?diff=174187&oldid=174144 5* 03Stegoratops 5* (+0) 10/* Calculator */ > 1769253665 670376 PRIVMSG #esolangs :14[[07Spam14]]4 10 02https://esolangs.org/w/index.php?diff=174188&oldid=122505 5* 03Cleverxia 5* (+2025) 10 > 1769255934 16299 PRIVMSG #esolangs :14[[07!!Fuck14]]4 10 02https://esolangs.org/w/index.php?diff=174189&oldid=140485 5* 03Cleverxia 5* (+2676) 10/* Examples */ > 1769256055 210462 PRIVMSG #esolangs :14[[07Talk:Combinatory logic14]]4 10 02https://esolangs.org/w/index.php?diff=174190&oldid=174186 5* 03Blashyrkh 5* (+426) 10/* What's the exact definition of cancellative combinator? */ new section > 1769258054 829437 PRIVMSG #esolangs :14[[07Programming abillities of different esolangs14]]4 M10 02https://esolangs.org/w/index.php?diff=174191&oldid=151623 5* 03Cleverxia 5* (+5448) 10this edit is mass language addition, supported by node.js and regex. revert if you thinks this is inappropirate, or you can add my name in the 'formatters' list. > 1769258240 164680 PRIVMSG #esolangs :14[[07Programming abillities of different esolangs14]]4 10 02https://esolangs.org/w/index.php?diff=174192&oldid=174191 5* 03Cleverxia 5* (-22159) 10removed the 'needs conversion', since the mass conversion is already done. revert the 2 edits if you think anything isn't appropriate > 1769260038 785216 PRIVMSG #esolangs :14[[07Programming abillities of different esolangs14]]4 M10 02https://esolangs.org/w/index.php?diff=174193&oldid=174192 5* 0347 5* (+72) 10 > 1769260229 582429 PRIVMSG #esolangs :14[[07Programming abillities of different esolangs14]]4 M10 02https://esolangs.org/w/index.php?diff=174194&oldid=174193 5* 0347 5* (-34) 10oh wait i didn't do anything, oops > 1769260683 423901 PRIVMSG #esolangs :14[[07!frjnrehrbwgyrigbyieurgbyfaerkhbvrwgtr.14]]4 M10 02https://esolangs.org/w/index.php?diff=174195&oldid=173544 5* 0347 5* (-289) 10 > 1769260708 828350 PRIVMSG #esolangs :14[[07!frjnrehrbwgyrigbyieurgbyfaerkhbvrwgtr.14]]4 M10 02https://esolangs.org/w/index.php?diff=174196&oldid=174195 5* 0347 5* (-14) 10/* Examples */ > 1769260964 411800 PRIVMSG #esolangs :14[[07!frjnrehrbwgyrigbyieurgbyfaerkhbvrwgtr.14]]4 M10 02https://esolangs.org/w/index.php?diff=174197&oldid=174196 5* 0347 5* (+18) 10 < 1769262504 623979 :amby!~ambylastn@host-81-178-158-197.as13285.net JOIN #esolangs amby :realname > 1769263268 774764 PRIVMSG #esolangs :14[[07User:Hotcrystal0/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=174198&oldid=174147 5* 03Hotcrystal0 5* (+108) 10 > 1769263967 371599 PRIVMSG #esolangs :14[[07User:Blashyrkh/Between IJ and SK14]]4 10 02https://esolangs.org/w/index.php?diff=174199&oldid=174185 5* 03Blashyrkh 5* (+1294) 10Beginning of the proof < 1769264775 340906 :impomatic!~impomatic@2a00:23c7:5fc6:3201:d844:8367:241f:5119 JOIN #esolangs * :[https://web.libera.chat] impomatic > 1769264799 912978 PRIVMSG #esolangs :14[[07Programming abillities of different esolangs14]]4 10 02https://esolangs.org/w/index.php?diff=174200&oldid=174194 5* 03I am islptng 5* (+172) 10add SLet > 1769264840 138096 PRIVMSG #esolangs :14[[07Programming abillities of different esolangs14]]4 M10 02https://esolangs.org/w/index.php?diff=174201&oldid=174200 5* 03I am islptng 5* (+2) 10fix > 1769265839 978727 PRIVMSG #esolangs :14[[07User:Blashyrkh/Between IJ and SK14]]4 10 02https://esolangs.org/w/index.php?diff=174202&oldid=174199 5* 03Blashyrkh 5* (+1123) 10a little more bit of the proof > 1769265917 836793 PRIVMSG #esolangs :14[[07Pain14]]4 M10 02https://esolangs.org/w/index.php?diff=174203&oldid=173645 5* 0347 5* (-638) 10 > 1769265985 618165 PRIVMSG #esolangs :14[[07Pain14]]4 M10 02https://esolangs.org/w/index.php?diff=174204&oldid=174203 5* 0347 5* (+0) 10 > 1769266017 564176 PRIVMSG #esolangs :14[[07Nope14]]4 10 02https://esolangs.org/w/index.php?diff=174205&oldid=172410 5* 03Yayimhere2(school) 5* (+6) 10 < 1769266328 342342 :DOS_User_webchat!~DOS_User_@user/DOS-User:11249 JOIN #esolangs DOS_User :[https://web.libera.chat] DOS_User_webchat > 1769266900 731382 PRIVMSG #esolangs :14[[07User:Blashyrkh/Between IJ and SK14]]4 M10 02https://esolangs.org/w/index.php?diff=174206&oldid=174202 5* 03Blashyrkh 5* (+621) 10 > 1769267476 761233 PRIVMSG #esolangs :14[[07User:Blashyrkh/Between IJ and SK14]]4 10 02https://esolangs.org/w/index.php?diff=174207&oldid=174206 5* 03Blashyrkh 5* (+61) 10/* Some ideas for the proof */ More strict definition of case 1 (to satisfy requirements of case 3) < 1769267575 342175 :DOS_User_webchat!~DOS_User_@user/DOS-User:11249 QUIT :Ping timeout: 272 seconds < 1769267634 351907 :DOS_User_webchat!~DOS_User_@user/DOS-User:11249 JOIN #esolangs DOS_User :[https://web.libera.chat] DOS_User_webchat < 1769267993 342530 :DOS_User_webchat!~DOS_User_@user/DOS-User:11249 QUIT :Ping timeout: 272 seconds < 1769268145 347691 :impomatic!~impomatic@2a00:23c7:5fc6:3201:d844:8367:241f:5119 QUIT :Ping timeout: 272 seconds < 1769269264 348704 :impomatic!~impomatic@2a00:23c7:5fc6:3201:d844:8367:241f:5119 JOIN #esolangs * :[https://web.libera.chat] impomatic < 1769272289 340575 :Yayimhere!~Yayimhere@197.185.190.142 JOIN #esolangs * :[https://web.libera.chat] Yayimhere < 1769272297 263513 :Yayimhere!~Yayimhere@197.185.190.142 PRIVMSG #esolangs :he-loooo < 1769273915 774752 :ehmry!~quassel@217.155.30.169 QUIT :Read error: Connection reset by peer > 1769276773 117625 PRIVMSG #esolangs :14[[07Bfppp14]]4 N10 02https://esolangs.org/w/index.php?oldid=174208 5* 03Sourceguy 5* (+691) 10Created page with "'''Bfppp''' is an esolang created by [[User:Sourceguy]]. It's an extension of Brainfuck. It contains a standard library, that makes coding in it a bit easier. == Instructions == '''Bfppp supports all Brainfuck instructions, and includes some new ones:''' * # - Commen > 1769276815 506242 PRIVMSG #esolangs :14[[07Bfppp14]]4 10 02https://esolangs.org/w/index.php?diff=174209&oldid=174208 5* 03Sourceguy 5* (+54) 10 > 1769276911 699586 PRIVMSG #esolangs :14[[07User:Sourceguy14]]4 10 02https://esolangs.org/w/index.php?diff=174210&oldid=136792 5* 03Sourceguy 5* (+12) 10 < 1769277093 799718 :Sgeo!~Sgeo@user/sgeo JOIN #esolangs Sgeo :realname > 1769279593 373996 PRIVMSG #esolangs :14[[07!frjnrehrbwgyrigbyieurgbyfaerkhbvrwgtr.14]]4 10 02https://esolangs.org/w/index.php?diff=174211&oldid=174197 5* 03Corbin 5* (+30) 10Tag slop. It's important to not let the design credit be reassigned from chatbots to humans. > 1769280480 947132 PRIVMSG #esolangs :14[[07Talk:Eodermdrome14]]4 10 02https://esolangs.org/w/index.php?diff=174212&oldid=59729 5* 03Yayimhere2(school) 5* (+299) 10/* Just making sure I understand */ new section > 1769280764 720031 PRIVMSG #esolangs :14[[07Talk:Eodermdrome14]]4 10 02https://esolangs.org/w/index.php?diff=174213&oldid=174212 5* 03Yayimhere2(school) 5* (+0) 10/* Just making sure I understand */ > 1769281174 17406 PRIVMSG #esolangs :14[[07Talk:Eodermdrome14]]4 10 02https://esolangs.org/w/index.php?diff=174214&oldid=174213 5* 03Yayimhere2(school) 5* (+238) 10 < 1769281201 45162 :Everything!~Everythin@172-232-54-192.ip.linodeusercontent.com JOIN #esolangs Everything :Everything > 1769281486 458186 PRIVMSG #esolangs :14[[07Set Trickery14]]4 N10 02https://esolangs.org/w/index.php?oldid=174215 5* 03A() 5* (+515) 10Created page with "Set Trickery is a set-based programming language that [[User:A()]] made. == Commands == {| class="wikitable" |+ Commands |- ! Command !! Explanation |- | (null) || empty set |- | (set{}) || set |- | (a/.../) || define a as ... |- | [a:b] || add a > 1769283118 817378 PRIVMSG #esolangs :14[[07Not My Type14]]4 N10 02https://esolangs.org/w/index.php?oldid=174216 5* 03Yayimhere2(school) 5* (+2301) 10Created page with "'''Not My Type''', named after its lack of actually being a type based language, yet still "claiming" to be, is an esoteric programming language created by [[User:Yayimhere]], based on the N -> (N -> N) type notation. == Definition == Not My > 1769283177 162834 PRIVMSG #esolangs :14[[07Not My Type14]]4 10 02https://esolangs.org/w/index.php?diff=174217&oldid=174216 5* 03Yayimhere2(school) 5* (-19) 10/* Definition */ > 1769283273 468976 PRIVMSG #esolangs :14[[07Not My Type14]]4 10 02https://esolangs.org/w/index.php?diff=174218&oldid=174217 5* 03Yayimhere2(school) 5* (+57) 10 > 1769283454 990157 PRIVMSG #esolangs :14[[07Not My Type14]]4 10 02https://esolangs.org/w/index.php?diff=174219&oldid=174218 5* 03Yayimhere2(school) 5* (+55) 10/* Example */ > 1769283486 459711 PRIVMSG #esolangs :14[[07Not My Type14]]4 10 02https://esolangs.org/w/index.php?diff=174220&oldid=174219 5* 03Yayimhere2(school) 5* (+1) 10/* See also */ < 1769283585 901384 :Lord_of_Life_!~Lord@user/lord-of-life/x-2819915 JOIN #esolangs Lord_of_Life :Lord < 1769283640 883252 :Lord_of_Life!~Lord@user/lord-of-life/x-2819915 QUIT :Ping timeout: 246 seconds > 1769283716 535392 PRIVMSG #esolangs :14[[07Special:Log/newusers14]]4 create10 02 5* 03Rainwave 5* 10New user account < 1769283753 430840 :Lord_of_Life_!~Lord@user/lord-of-life/x-2819915 NICK :Lord_of_Life > 1769283904 581187 PRIVMSG #esolangs :14[[07Not My Type14]]4 10 02https://esolangs.org/w/index.php?diff=174221&oldid=174220 5* 03Yayimhere2(school) 5* (+50) 10/* Definition */ > 1769283968 634465 PRIVMSG #esolangs :14[[07Not My Type14]]4 10 02https://esolangs.org/w/index.php?diff=174222&oldid=174221 5* 03Yayimhere2(school) 5* (+43) 10/* Definition */ > 1769283988 87597 PRIVMSG #esolangs :14[[07Not My Type14]]4 10 02https://esolangs.org/w/index.php?diff=174223&oldid=174222 5* 03Yayimhere2(school) 5* (+8) 10/* Example */ < 1769284035 875756 :Yayimhere!~Yayimhere@197.185.190.142 QUIT :Quit: Client closed < 1769284353 976994 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name) < 1769284402 306288 :jinn6!jan6@tilde.team/user/jan6 JOIN #esolangs jinn6 :genThey're Advocatus Diaboli < 1769284606 809822 :chloetax!~chloe@user/chloetax QUIT :Ping timeout: 246 seconds > 1769284651 857457 PRIVMSG #esolangs :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=174224&oldid=174132 5* 03Rainwave 5* (+227) 10/* Introductions */ > 1769284659 492300 PRIVMSG #esolangs :14[[0714]]4 10 02https://esolangs.org/w/index.php?diff=174225&oldid=120509 5* 03Yayimhere2(school) 5* (+0) 10/* Overview */ > 1769285236 828587 PRIVMSG #esolangs :14[[07Talk:14]]4 10 02https://esolangs.org/w/index.php?diff=174226&oldid=82273 5* 03Yayimhere2(school) 5* (+282) 10/* turing completeness? */ new section > 1769285525 398415 PRIVMSG #esolangs :14[[07Talk:Eodermdrome14]]4 10 02https://esolangs.org/w/index.php?diff=174227&oldid=174214 5* 03Keymaker 5* (+212) 10Graphs. > 1769285555 2085 PRIVMSG #esolangs :14[[07User:Blashyrkh/Between IJ and SK14]]4 10 02https://esolangs.org/w/index.php?diff=174228&oldid=174207 5* 03Blashyrkh 5* (+213) 10/* Some ideas for the proof */ The program has found a really tough case > 1769285604 718708 PRIVMSG #esolangs :14[[07User:Yayimhere14]]4 10 02https://esolangs.org/w/index.php?diff=174229&oldid=174172 5* 03Yayimhere2(school) 5* (-86) 10/* esolangs */ > 1769286205 969288 PRIVMSG #esolangs :14[[07User talk:Blashyrkh/Between IJ and SK14]]4 10 02https://esolangs.org/w/index.php?diff=174230&oldid=174183 5* 03Blashyrkh 5* (+148) 10/* Does John Tromp know the answer? */ new section > 1769286243 983721 PRIVMSG #esolangs :14[[07User talk:Blashyrkh/Between IJ and SK14]]4 M10 02https://esolangs.org/w/index.php?diff=174231&oldid=174230 5* 03Blashyrkh 5* (+91) 10 > 1769286854 715861 PRIVMSG #esolangs :14[[07Esolang:Introduce yourself14]]4 M10 02https://esolangs.org/w/index.php?diff=174232&oldid=174224 5* 03LeCo13 5* (+168) 10 > 1769286897 519401 PRIVMSG #esolangs :14[[07SSEG14]]4 N10 02https://esolangs.org/w/index.php?oldid=174233 5* 03LeCo13 5* (+1066) 10Created page with "SEG or SSEG is an programming language written in only 1s and 0s made by laptopcoder11 ''(idk how to properly make pages, so pls improve if u can)'' instructions: {| class="wikitable" |- ! instruction !! functionality |- | 000n || decrease register-n |- | 0 < 1769288364 341566 :APic!apic@apic.name PRIVMSG #esolangs :cu < 1769288700 89678 :chloetax!~chloe@user/chloetax JOIN #esolangs chloetax :chloe < 1769291749 348053 :Everything!~Everythin@172-232-54-192.ip.linodeusercontent.com QUIT :Quit: leaving > 1769294785 326015 PRIVMSG #esolangs :14[[07ELBOG14]]4 M10 02https://esolangs.org/w/index.php?diff=174234&oldid=135737 5* 03CPNK 5* (+100) 10add xkcd random number, change ref interpreter url > 1769295944 418726 PRIVMSG #esolangs :14[[07Backtick14]]4 10 02https://esolangs.org/w/index.php?diff=174235&oldid=172577 5* 03Splot-dev 5* (+694) 10Added library example. > 1769296085 547551 PRIVMSG #esolangs :14[[07Backtick14]]4 M10 02https://esolangs.org/w/index.php?diff=174236&oldid=174235 5* 03Splot-dev 5* (+12) 10Fixed wording. > 1769296143 357568 PRIVMSG #esolangs :14[[07Backtick14]]4 M10 02https://esolangs.org/w/index.php?diff=174237&oldid=174236 5* 03Splot-dev 5* (-1) 10More wording fixed. > 1769296196 345262 PRIVMSG #esolangs :14[[07Backtick14]]4 M10 02https://esolangs.org/w/index.php?diff=174238&oldid=174237 5* 03Splot-dev 5* (+29) 10changed code - added comment to Libraries section code < 1769297622 965380 :Sgeo!~Sgeo@user/sgeo PRIVMSG #esolangs :https://www.reddit.com/r/math/comments/18gs6cr/unprovability_vs_independence/ < 1769298819 694109 :TheHermit108!~TheHermit@user/TheHermit108 JOIN #esolangs TheHermit108 :realname < 1769298862 849398 :TheHermit108!~TheHermit@user/TheHermit108 PART #esolangs :Leaving