BusyBeaver(5) is now known to be 47,176,870
The news these days feels apocalyptic to me—as if we’re living through, if not the last days of humanity, then surely the last days of liberal democracy on earth.
All the more reason to ignore all of that, then, and blog instead about the notorious Busy Beaver function! Because holy moly, what news have I got today. For lovers of this super-rapidly-growing sequence of integers, I’ve honored to announce the biggest Busy Beaver development that there’s been since 1983, when I slept in a crib and you booted up your computer using a 5.25-inch floppy. That was the year when Allen Brady determined that BusyBeaver(4) was equal to 107. (Tibor Radó, who invented the Busy Beaver function in the 1960s, quickly proved with his student Shen Lin that the first three values were 1, 6, and 21 respectively. The fourth value was harder.)
Only now, after an additional 41 years, do we know the fifth Busy Beaver value. Today, an international collaboration called bbchallenge is announcing that it’s determined, and even formally verified using the Coq proof system, that BB(5) is equal to 47,176,870—the value that’s been conjectured since 1990, when Heiner Marxen and Jürgen Buntrock discovered a 5-state Turing machine that runs for exactly 47,176,870 steps before halting, when started on a blank tape. The new bbchallenge achievement is to prove that all 5-state Turing machines that run for more steps than 47,176,870, actually run forever—or in other words, that 47,176,870 is the maximum finite number of steps for which any 5-state Turing machine can run. That’s what it means for BB(5) to equal 47,176,870.
For more on this story, see Ben Brubaker’s superb article in Quanta magazine, or bbchallenge’s own announcement. For more background on the Busy Beaver function, see my 2020 survey, or my 2017 big numbers lecture, or my 1999 big numbers essay, or the Googology Wiki page, or Pascal Michel’s survey.
The difficulty in pinning down BB(5) was not just that there are a lot of 5-state Turing machines (16,679,880,978,201 of them to be precise, although symmetries reduce the effective number). The real difficulty is, how do you prove that some given machine runs forever? If a Turing machine halts, you can prove that by simply running it on your laptop until halting (at least if it halts after a “mere” ~47 million steps, which is child’s-play). If, on the other hand, the machine runs forever, via some never-repeating infinite pattern rather than a simple infinite loop, then how do you prove that? You need to find a mathematical reason why it can’t halt, and there’s no systematic method for finding such reasons—that was the great discovery of Gödel and Turing nearly a century ago.
More precisely, the Busy Beaver function grows faster than any function that can be computed, and we know that because if a systematic method existed to compute arbitrary BB(n) values, then we could use that method to determine whether a given Turing machine halts (if the machine has n states, just check whether it runs for more than BB(n) steps; if it does, it must run forever). This is the famous halting problem, which Turing proved to be unsolvable by finite means. The Busy Beaver function is Turing-uncomputability made flesh, a finite function that scrapes the edge of infinity.
There’s also a more prosaic issue. Proofs that particular Turing machines run forever tend to be mind-numbingly tedious. Even supposing you’ve found such a “proof,” why should other people trust it, if they don’t want to spend days staring at the outputs of your custom-written software?
And so for decades, a few hobbyists picked away at the BB(5) problem. One, who goes by the handle “Skelet”, managed to reduce the problem to 43 holdout machines whose halting status was still undetermined. Or maybe only 25, depending who you asked? (And were we really sure about the machines outside those 43?)
The bbchallenge collaboration improved on the situation in two ways. First, it demanded that every proof of non-halting be vetted carefully. While this went beyond the original mandate, a participant named “mxdys” later upped the standard to fully machine-verifiable certificates for every non-halting machine in Coq, so that there could no longer be any serious question of correctness. (This, in turn, was done via “deciders,” programs that were crafted to recognize a specific type of parameterized behavior.) Second, the collaboration used an online forum and a Discord server to organize the effort, so that everyone knew what had been done and what remained to be done.
Despite this, it was far from obvious a priori that the collaboration would succeed. What if, for example, one of the 43 (or however many) Turing machines in the holdout set turned out to encode the Goldbach Conjecture, or one of the other great unsolved problems of number theory? Then the final determination of BB(5) would need to await the resolution of that problem. (We do know, incidentally, that there’s a 27-state Turing machine that encodes Goldbach.)
But apparently the collaboration got lucky. Coq proofs of non-halting were eventually found for all the 5-state holdout machines.
As a sad sidenote, Allen Brady, who determined the value of BB(4), apparently died just a few days before the BB(5) proof was complete. He was doubtful that BB(5) would ever be known. The reason, he wrote in 1988, was that “Nature has probably embedded among the five-state holdout machines one or more problems as illusive as the Goldbach Conjecture. Or, in other terms, there will likely be nonstopping recursive patterns which are beyond our powers of recognition.”
Maybe I should say a little at this point about what the 5-state Busy Beaver—i.e., the Marxen-Buntrock Turing machine that we now know to be the champion—actually does. Interpreted in English, the machine iterates a certain integer function g, which is defined by
- g(x) = (5x+18)/3 if x = 0 (mod 3),
- g(x) = (5x+22)/3 if x = 1 (mod 3),
- g(x) = HALT if x = 2 (mod 3).
Starting from x=0, the machine computes g(0), g(g(0)), g(g(g(0))), and so forth, halting if and if it ever reaches … well, HALT. The machine runs for millions of steps because it so happens that this iteration eventually reaches HALT, but only after a while:
0 → 6 → 16 → 34 → 64 → 114 → 196 → 334 → 564 → 946 → 1584 → 2646 → 4416 → 7366 → 12284 → HALT.
(And also, at each iteration, the machine runs for a number of steps that grows like the square of the number x.)
Some readers might be reminded of the Collatz Conjecture, the famous unsolved problem about whether, if you repeatedly replace a positive integer x by x/2 if x is even or 3x+1 if x is odd, you’ll always eventually reach x=1. As Scott Alexander would say, this is not a coincidence because nothing is ever a coincidence. (Especially not in math!)
It’s a fair question whether humans will ever know the value of BB(6). Pavel Kropitz discovered, a couple years ago, that BB(6) is at least 10^10^10^10^10^10^10^10^10^10^10^10^10^10^10 (i.e., 10 raised to itself 15 times). Obviously Kropitz didn’t actually run a 6-state Turing machine for that number of steps until halting! Instead he understood what the machine did—and it turned out to apply an iterative process similar to the g function above, but this time involving an exponential function. And the process could be proven to halt after ~15 rounds of exponentiation.
Meanwhile Tristan Stérin, who coordinated the bbchallenge effort, tells me that a 6-state machine was recently discovered that “iterates the Collatz-like map {3x/2, (3x-1)/2} from the number 8 and halts if and only if the number of odd terms ever gets bigger than twice the number of even terms.” This shows that, in order to determine the value of BB(6), one would first need to prove or disprove the Collatz-like conjecture that that never happens.
Basically, if and when artificial superintelligences take over the world, they can worry about the value of BB(6). And then God can worry about the value of BB(7).
I first learned about the BB function in 1996, when I was 15 years old, from a book called The New Turing Omnibus by A. K. Dewdney. From what I gather, Dewdney would go on to become a nutty 9/11 truther. But that’s irrelevant to the story. What matters was that his book provided my first exposure to many of the key concepts of computer science, and probably played a role in my becoming a theoretical computer scientist at all.
And of all the concepts in Dewdney’s book, the one I liked the most was the Busy Beaver function. What a simple function! You could easily explain its definition to Archimedes, or Gauss, or any of the other great mathematicians of the past. And yet, by using it, you could name definite positive integers (BB(10), for example) incomprehensibly larger than any that they could name.
It was from Dewdney that I learned that the first four Busy Beaver numbers were the unthreatening-looking 1, 6, 21, and 107 … but then that the fifth value was already unknown (!!), and at any rate at least 47,176,870. I clearly remember wondering whether BB(5) would ever be known for certain, and even whether I might be the one to determine it. That was almost two-thirds of my life ago.
As things developed, I played no role whatsoever in the determination of BB(5) … except for this. Tristan Stérin tells me that reading my survey article, The Busy Beaver Frontier, was what inspired him to start and lead the bbchallenge collaboration that finally cracked the problem. It’s hard to express how gratified that makes me.
Why care about determining particular values of the Busy Beaver function? Isn’t this just a recreational programming exercise, analogous to code golf, rather than serious mathematical research?
I like to answer that question with another question: why care about humans landing on the moon, or Mars? Those otherwise somewhat arbitrary goals, you might say, serve as a hard-to-fake gauge of human progress against the vastness of the cosmos. In the same way, the quest to determine the Busy Beaver numbers is one concrete measure of human progress against the vastness of the arithmetical cosmos, a vastness that we learned from Gödel and Turing won’t succumb to any fixed procedure. The Busy Beaver numbers are just … there, Platonically, as surely as 13 was prime long before the first caveman tried to arrange 13 rocks into a nontrivial rectangle and failed. And yet we might never know the sixth of these numbers and only today learned the fifth.
Anyway, huge congratulations to the bbchallenge team on their accomplishment. At a terrifying time for the world, I’m happy that, whatever happens, at least I lived to see this.
Follow
Comment #1 July 2nd, 2024 at 10:12 am
It’s even more remarkable to me that the proof is verified using an automatic proof system. I think such systems do not receive much attention from the AI community (for better or worse). It’s when they become an integral part of AI systems that we should start counting the days before the apocalypse. AlphaGeometry is the first sign of that.
Comment #2 July 2nd, 2024 at 10:28 am
[…] and is filed underneath Bulletins, Complexity. You may observe any responses to this entry by the RSS 2.0 […]
Comment #3 July 2nd, 2024 at 11:30 am
Shouldn’t g(x)’s definition be based on whether x (the input), rather than g(x) is a certain mod 3?
Comment #4 July 2nd, 2024 at 11:37 am
lewikee #3: Duhhhh, thanks, fixed!
Comment #5 July 2nd, 2024 at 11:37 am
I also found about BB a long time ago from reading a french book that compiled a series of K.Dewdney’s columns from Scientific American.
Although all the articles were fascinating, I remember that the one about the Mandelbrot set was the one I preferred
http://miriam-english.org/files/Dewdney_Mandelbrot/Dewdney_Mandelbrot.html
And generating the images was feasible even with a very limited 1980s computer, it was just a question of patience.
Comment #6 July 2nd, 2024 at 12:12 pm
I don’t see how anyone could argue this is more frivolous than the vast majority of theoretical math.
Comment #7 July 2nd, 2024 at 12:25 pm
The survey was a big inspiration to me too! It was a big success — so successful indeed that it is now hopelessly out of date. Maybe time for an updated version?
Comment #8 July 2nd, 2024 at 12:30 pm
There’s an even bigger developing story around the Busy Beaver challenge in my competely unqualified opinion. As of June 28, it appears they’ve now found a Collatz-like TM in BB(6,2), B(3,3), and BB(2,5). (The second number is the number of symbols, so BB(6)=BB(6,2).) This is the entire easiest frontier of BB(x,y), so we’re now locked in by Collatz-like “Cryptids”. “Antihydra”, “Bigfoot”, and “Hydra”, which all appear to not halt, but to prove it, they’d need to prove something Collatz-like. Collatz-like in BB(6) alone is huge news imo.
Comment #9 July 2nd, 2024 at 12:37 pm
Andrew McKnight #6: Yes, I talked about the new Collatz-like 6-state machine in the post!
Comment #10 July 2nd, 2024 at 12:45 pm
Pete #6:
I don’t see how anyone could argue this is more frivolous than the vast majority of theoretical math.
I’ve been a big supporter and defender of Busy Beaver and other “recreational math” topics for 25 years. I understand the snobbish perspective, which cares only about how much a given topic draws on and/or contributes to the central technical directions of the field, a criterion where BusyBeaverology does less well. It’s just that I also factor in: how cool is this? How many nerdy kids will it excite? Was great ingenuity and effort expended, even if not the kinds that we usually value? Were strange new creatures brought back for examination from the Platonic wilderness?
And also, in this case, if nothing else: what a phenomenal demonstration of the power of formal verification with Coq!
Comment #11 July 2nd, 2024 at 12:48 pm
Nick Drozd #7: Thanks so much! But eh, I’d prefer to do something new if and when I return to this topic … like what about a paper on Lazy Beavers, or Beeping Busy Beavers? 😉
Comment #12 July 2nd, 2024 at 12:55 pm
I wonder if there’s any cryptographic use for the halting problem. Especially since BB gives you a choice between the brute force and the structure exploitation
Comment #13 July 2nd, 2024 at 1:14 pm
Long-time reader, first-time commenter.
I read your very early piece on “who can name the bigger number” when I was in high school and first stumbled on your blog and writings. The concept of busy beaver numbers, to this young nerd, was so awe-inspiring and so far outside of the math and programming I had been exposed to by then. I was instantly seduced by it—by the realization that computation is somehow fundamental to mathematics itself. I credit reading this piece, and other of your blog posts, with inspiring me to pursue a very successful career as a software engineer—in my job I’ve been able to apply a lot of interesting results from algorithm theory, so I consider myself somewhat of an “industry theorist.”
I’m commenting now because I’m disturbed by the exclusionary tone of many of your recent posts, and I’m worried that your blog has become no longer a “safe space” for young nerds who have different political beliefs than you. I’m a massive fan of Trump and admire what he’s done for our country, and I’m volunteering for his campaign this summer. Your hostile posts and comments towards Trump supporters I’m finding increasingly hostile. You run the risk of pushing away young nerdy Trump fans who could otherwise be inspired by you. So, I implore you: please stop talking about politics. Please stop saying negative things about Trump and criticizing him on your blog.
Comment #14 July 2nd, 2024 at 1:22 pm
Scott
“How many nerdy kids will it excite?”
Exactly! This is about inspiring kids.
Then some kids get so excited, they never get over it (like all the people still working on BB).
Comment #15 July 2nd, 2024 at 1:31 pm
I’m a little surprised to find you, of all people, defending Platonism. 13 being prime might not be (necessarily) a claim about arranging rocks into non-trivial rectangles, but why is it not a claim about the (still physical) process of symbol manipulation? I find it particularly ironic to see Platonism defended in the context of a discussion of Turing machines, because the *whole point* of Turing machines as a computational model is that they have a more straightforward physical realization than, say, the lambda calculus.
Comment #16 July 2nd, 2024 at 1:35 pm
> It’s just that I also factor in: how cool is this? How many nerdy kids will it excite? Was great ingenuity and effort expended, even if not the kinds that we usually value? Were strange new creatures brought back for examination from the Platonic wilderness?
Amen!
I think the Smith aperiodic tile (hat) discovery was also of this flavor, as were many of the things John Conway did (in addition to his massive contributions to “central technical directions” of math research).
There’s just something so delightful about this stuff.
Comment #17 July 2nd, 2024 at 2:17 pm
Ron Garret #15: I’ve often described myself, including on this blog, as “a Platonist about arithmetic (or anything that’s ultimately reducible to the behavior of Turing machines), and a formalist about everything else.” Some people refuse to be Platonists even about arithmetic—holding, e.g., that whether a given Turing machine halts or runs forever, or whether Goldbach’s Conjecture holds, could depend on the laws of physics (!). I’ve never been able to make sense of that position. But I’m happy to be a formalist about the Continuum Hypothesis, Axiom of Choice, and the like, and just study the whole multiverse of possibilities there.
Comment #18 July 2nd, 2024 at 2:18 pm
Very cool seeing this news. It kind of reminds me of one of my favorite TV shows growing up, Connections by James Burke. If you’ve never seen this show, it’s about how changes in society or inventions are often caused by other inventions with apparently little in common.
BB(5) is so complex to prove that a single person or group could not come up with a proof. Instead, they needed to split it up into millions of sub-problems so that the work could be efficiently distributed. This creates a new problem: how can you trust work from people you don’t know? You need to first invent computer aided proof verification, because you can’t hand-check a million proofs.
You also need social technology, to organize the project, and keep people excited about it. You need this because nobody is going to fund work on this. If it’s going to be solved, then the idea needs to be interesting enough and the community needs to be engaging enough that people keep coming back, and you need to avoid duplicating work across millions of problems.
The most exciting idea that Connections left me with is the idea of latent inventions: inventions where all the prerequisite technologies have been invented, but nobody has realized yet that these innovations across three unrelated fields can combine into a new invention. Often this takes quite a while – it is easy to look back and find a technology’s dependencies, but much harder to look forward and realize what its dependents will be.
Comment #19 July 2nd, 2024 at 3:05 pm
Scott #10, Pete #6: Which areas of theoretical math are most likely to be useless? What would you cut if you were head of the NSF and cuts were necessary?
Comment #20 July 2nd, 2024 at 3:14 pm
[…] Article URL: https://scottaaronson.blog/?p=8088 […]
Comment #21 July 2nd, 2024 at 3:48 pm
This made me wonder, are there variants of the BB function that are not defined in terms of Turing machines, but in terms of other models of computation, e.g. lambda calculus? And if so, can the result for BB(5) be translated and used for those other functions? If the reference to Turing machines is not essential, this would give additional credence to the importance of the result. Perhaps similar to how we care more about mathematical patterns in arithmetic that don’t just apply to base 10.
Comment #22 July 2nd, 2024 at 4:58 pm
Anon
“Which areas of theoretical math are most likely to be useless?”
Maybe the kind of math that posits clearly nonsensical stuff?
“Let’s suppose for a second that there’s such a thing as the square root of -1”
😛
Comment #23 July 2nd, 2024 at 5:36 pm
@Max #21
“This made me wonder, are there variants of the BB function that are not defined in terms of Turing machines, but in terms of other models of computation, e.g. lambda calculus? And if so, can the result for BB(5) be translated and used for those other functions?”
You can define something similar for pretty much whatever your preferred Turing complete formalism is. However, Turing machines are one of the simplest such an therefore one of the easies to analyze. It is unlikely that this sort of result can translate much usefully into other Turing complete settings. A lower bound on a specific Busy Beaver value for Turing machines will translate into a lower bound on an analogous function for any other system, but because there’s so much overhead in modeling Turing machines with one system or another, or using Turing machines to model another, upper bounds on BB are unlikely to tell you much at all about any other system.
Comment #24 July 2nd, 2024 at 5:54 pm
Anon #19: “Which areas of theoretical math are most likely to be useless? What would you cut if you were head of the NSF and cuts were necessary?”
The really useless math is where the NSF doesn’t need to cut anything. For example, ever heard of finite projective (plane) geometry? The conjecture is that the only orders for which there is a projective plane of order n is when n is a prime number to some positive integer power. Currently, the lowest order for which the conjecture has not been proven is 12.
Or looking for purely algebraic proofs of well-known stuff, just because they are guaranteed to exist, and you want to know how trivial or complicated they are. (I once played around with the-E-theorem-prover and prover9, as well as prover9’s companion program mace4, which finds counterexamples.)
Comment #25 July 2nd, 2024 at 6:04 pm
Anon #19:
Which areas of theoretical math are most likely to be useless?
Oh, they’re all pretty useless. 😀
What would you cut if you were head of the NSF and cuts were necessary?
I could probably find some superfluous facility earmarked by Congress, because it was located in the appropriation committee chair’s state, that cost more than all the theoretical math research combined.
Comment #26 July 2nd, 2024 at 7:02 pm
I should have asked you this BEFORE B(5) is known, but I will ask it anyway: Lets say one showed that if you find B(5) you find if Goldback is True or False. You seem to say this is a reason to think we will never find B(5). Could one instead say that its a reason to want to find B(5)?
That is, just because solving X wouls solve an important unsolved problems might not mean that you shouldn’t work on X. Especially for BB since a proof of Goldback via BB would prob be very different than a proof of X via normal Number Theory.
Comment #27 July 2nd, 2024 at 8:05 pm
William Gasarch #26: No. In practice, answering all possible arithmetical questions that can be encoded by n-state machines is how you find out the value of BB(n). Starting from BB would be like trying to win the Olympics by asking yourself, “assume I have a gold medal; now what did I do to get it?”
Comment #28 July 2nd, 2024 at 8:17 pm
Why not now use the known bb number(turing) machines to create a minimal set language compute language that we know would halt
Basically we have turing machines we know will halt – use those as compute blocks/functions. If we discover provable halting ones in bb(6) we have a more expressive language. If I’m understanding it right these would be the minimal k-complexity programs from a bottom up approach (as opposed to compression)
Comment #29 July 2nd, 2024 at 8:24 pm
Lloth #28: I mean, you could do that, but how much is it good for? We now have a complete listing of Turing machines with 2 symbols and up to 5 states that halt on an initially blank tape. In practical programming, one usually cares more about routines that halt on all inputs (which is a different question), and almost all the routines one would care about would have far more than 5 states when compiled down to Turing machine.
Comment #30 July 2nd, 2024 at 9:15 pm
As a nonexpert, merely thinking things through, the use might be academic – and put things on firm grounding, a blossoming pure flower, not necessarily a functional one, not yet anyway. The point being not actually program – but to see what can be done with what remains. Idle curiosity is all.
Comment #31 July 2nd, 2024 at 9:25 pm
I think the collatz-like cryptid “Antihydra” can be simplified to A061418 in the OEIS if the description you provided is accurate – If you consider the numbers in binary, what Antihydra does is it takes a number, shifts it one bit to the right while cutting off the last digit, and then adds it to the original. There are some details missing from that analysis, but it doesn’t fundamentally change the problem, just some things with the last digit. Then, the question is whether there are twice as many odds in A061418 as evens at any point.
Comment #32 July 3rd, 2024 at 5:39 am
[…] is filed under Announcements, Complexity. You can follow any responses to this entry through the RSS 2.0 […]
Comment #33 July 3rd, 2024 at 6:12 am
The Busy Beaver is definitely a cool topic. Two (long-term) research agendas that come to mind:
1) Clarifying relations between the hierarchy of large cardinal axioms, and the Busy Beaver hierarchy. Large cardinal axioms in transfinite set theory form a strict hierarchy of increasing logical strength – the higher you go, the more you can prove. But one can find concrete mathematical problems whose truth or falsehood depends on the large cardinal axioms. In particular, you can construct a Turing machine which halts only if a given large cardinal axiom is true. One can then ask, what are the lowest BB numbers that can only be determined through the use of a given large cardinal axiom? (I know Scott has worked on a similar topic.)
2) Doing the same thing for other classes of problems. For example, it seems like “Collatz-like problems” might also admit of a similar hierarchical classification.
Comment #34 July 3rd, 2024 at 7:11 am
Upon reflection, the obvious solution would have a superset changing the input tape, so bb(5,2,1), and have the zero tape input be a special case, and continue the great works from there.
Comment #35 July 3rd, 2024 at 7:14 am
This is incredible! Congratulations to the team that worked so hard on this! Woohooooo!!!!
Comment #36 July 3rd, 2024 at 7:31 am
Hi Scott: great article. I love the BB function, which I learned in your Democritus book: truly fascinating. I’m not a computer scientist though and sorry if I ask something really silly.
1) The Turing machine has an infinite tape. With a finite tape it becomes a finite automata, you can always verify if it halts or not, so there is no halting problem. Is this correct?
2) The finiteness of the tape looks like if I take only a finite subset of the integers, so also the Gödel’s theorems do not apply, since you havre to be able to define infinite induction.
Conclusion: since effectively we use only finite numbers, are halting, Goedel and non-computable functions really something important for understating out world? Or, if you like, is all this relevant for physics? I tried to solve all this by myself since a while but I would really hear the opinion of an expert. I have this constant suspect that all this comes from considering infinite sets. Thanks for any comment on this!
Comment #37 July 3rd, 2024 at 8:49 am
LK2 #36: Certainly, if you have a tape of bounded size, then the BB function becomes computable (quickly hitting a ceiling that’s exponential in the number of tape squares) and Gödel incompleteness no longer applies.
Does that make the BB function “irrelevant for physics”? Well, I dunno! The function exp(exp(n)) could already be argued to be “irrelevant for physics” on much the same grounds.
Also, BB(5) (as we know now) is “merely” 47,176,870, which fits not merely in the observable universe but in your phone. BB(6) would not fit in the observable universe if written in any standard notation, but on the other hand, we, living in the observable universe, managed to figure that out, which imbues the fact with a certain physical reality, doesn’t it? 😉
Comment #38 July 3rd, 2024 at 9:10 am
Scott, first thank you very much for your answer!
Probably my question boils down to: do Gödel’s theorems and Turing machines have any relevance for physics? I understand that both tell us something about some formal systems and this has some relevance, but if someone (ok, not me) would like to discard “infinities”, then all this doesn’t not apply or at least it has relevance for math and philosophy “only”.
I’d like to re-state that I’m not rejecting computability theory or mathematical logic results: my questions are intended for me to understand all that more deeply and to understand if there are any reflections of all this in physics. For me it is easier to understand the relevance of complexity theory (solve NP-complete problems in poly time –> not physical, just to badly summarise, or non-linearity in QM –> solve NP-complete problems etc…) to physics than this.
And yes, your last sentence gives me something interesting to think about 😉
Thanks again.
Comment #39 July 3rd, 2024 at 9:29 am
Scott #37
“The function exp(exp(n)) could already be argued to be “irrelevant for physics” on much the same grounds.”
those are obviously not the type of unbounded growth implied by BB, but double exponential models apparently do show up in biology and physics
https://pubs.acs.org/doi/abs/10.1021/ja00113a005
Comment #40 July 3rd, 2024 at 9:49 am
Pete #6 wrote: “I don’t see how anyone could argue this is more frivolous than the vast majority of theoretical math.”
I easily could! It’s a result that is unlikely to have major consequences for other topics in mathematics or computer science. It’s more like computing the 100 trillionth decimal digit of pi (which by the way is zero – all that work for nothing!) than proving some seemingly obscure result that has a decent chance of feeding back into the grand structure of mathematics.
But I don’t like the word “frivolous” here – I’d say “recreational”. And I’m very much against complaining about recreational mathematics. It’s like coming out against fun. And the quest for BB(5) was quite exciting to me.
Comment #41 July 3rd, 2024 at 10:16 am
LK2 Says #38: “Probably my question boils down to: do Gödel’s theorems and Turing machines have any relevance for physics? I understand that both tell us something about some formal systems and this has some relevance, but if someone (ok, not me) would like to discard “infinities”, then all this doesn’t not apply …”
Randomness has relevance for physics. Maybe you could somehow discard “infinities” and still work with randomness, but it is not obvious (to me) how. On the other hand, all those hierarchies of unsolvable problemes gives you nice relative notions of randomness. And some of the hardest “important” problems in mathematics, like the Riemann hypothesis, have close connections to randomness too.
Comment #42 July 3rd, 2024 at 10:41 am
LK2 #38: What I’m trying to explain is that there’s not a natural category of “the math that’s relevant for physics,” with everything outside the charmed circle consigned to eternal irrelevance. Math is shot through with unexpected connections. Many mathematical topics, from complex numbers to Riemannian geometry to non-abelian groups, famously seemed irrelevant to physics at first but then became relevant later.
I can’t make a case that physicists will ever need to know specific values of the BB function—even when those values are “merely” in the millions like BB(5), let alone when they’re hyper-mega-astronomical like BB(6). More broadly, though, physicists are exceedingly interested in understanding how complex behavior emerges out of simple deterministic rules. And the Busy Beaver game has been, in my view, one of the most beautiful testbeds for investigating that question since it was invented 60 years ago.
Comment #43 July 3rd, 2024 at 10:53 am
As to the “frivolity” of such topics, I am reminded of the editorial comment in Johnson and Story’s 1879 parity-argument proof partitioning the configurations of the 15-puzzle.
Apparently the editors were concerned, even in the late 19th century, that the then-new *American Journal of Mathematics* would be seen as focusing on trivialities, but they defended themselves in a footnote by noting the relationship between the 15-puzzle and its relation to abstract algebra:
Comment #44 July 3rd, 2024 at 12:38 pm
This is great, but isn’t there a lot of variation in exactly which Turing machines you’re interested in? Andrew McKnight already mentioned that BB(5) is shorthand for BB(5, 2), meaning binary symbols, but we could be exploring ternary or more symbols. Also, there could be BB(5, tape=10^10), meaning a finite tape with 10^10 cells (with variants for whether the tape is circular, or whether you halt or just don’t move when you hit the edge), or BB(5, heads=2) meaning two parallel read/write heads, or BB(5, stochastic=True) meaning that some rules have stochastic outputs or actions, etc. All these things can be simulated with a finite-sized interpreter, so normally we don’t care about the differences, but if you’re interested in strictly limited machines (e.g. BB(5) versus BB(6)) then these details matter.
Comment #45 July 3rd, 2024 at 12:44 pm
Peter Norvig #44: Sure, you can study any of those variants—and if you look at e.g. bbchallenge.org or Pascal Michel’s survey, you’ll see that many people do! (Especially the variants involving more tape symbols.)
For me, though, the original function defined by Tibor Rado in 1962 (specifically, what he called the “shift function” S(n), but I simply call BB(n)) will always have a special place, just like the original rules of chess compared to the thousands of fairy chess variants. 🙂
Comment #46 July 3rd, 2024 at 3:40 pm
@Max #21
Yes, there is a functional busy beaver defined in terms of the lambda calculus [1]. Since it measures program size in bits rather than states, it allows many more values to be determined (37 so far versus only 6 for TMs, with no behaviour in common whatsoever), and the gap between the largest known value and values beyond Graham’s Number is a mere 13 program bits. A closely related variant [2] can be directly expressed in terms of Kolmogorov complexity, which Mikhail Andreev argues [3] is crucial for applications in Information Theory.
[1] https://oeis.org/A333479
[2] https://oeis.org/A361211
[3] https://arxiv.org/pdf/1703.05170
Comment #47 July 3rd, 2024 at 4:48 pm
I have a stupid question.
Obviously, the BB function is not computable because if it was you could solve the halting problem. You reformulate that in this way: “there exists no systematic method to show if a turing machine halts”.
This makes it sound that in order to compute BB, you would have to solve infinite many “non isomorphic” problems showing that some specific turing machine does not halt.
My question is, could it be that it is just strictly impossible to show that some turing machine does not halt for a given n? As in, there exists a specific turing machine such that no proof can show that it does not halt? Shouldn’t the first n with that property be interesting?
I suppose, you wouldn’t even be able to prove its existence though, as you cannot prove that an undecidable statement is undecidable internally.
Comment #48 July 3rd, 2024 at 4:59 pm
Do we know anything about these Turing machines considered as functions? Like, the Marxen-Buntrock Turing machine iterates g starting at 0. With other inputs (that is, initial conditions of the tape), does it still iterate g, but starting at a different number? Or does it do something else entirely?
It’s kind of interesting that a Turing machine “really” implements a partial function t(x), but for the Busy Beaver challenge we have to restrict it to t(0), I guess because arbitrarily high runtimes are achievable with different inputs. I suppose we would have to redo all the work if we defined a new challenge where the tapes start with a 1 at the initial position of the head.
Comment #49 July 3rd, 2024 at 5:07 pm
Random #47: LOL, Adam Yedidia and I wrote a whole paper on that exact question 8 years ago!
Long story short, for any fixed axiomatic system F, yes, you can construct a Turing machine that loops through all theorems of F, halting if and only if finds a contradiction. If F is consistent, then that machine runs forever, but the fact that it does so is unprovable in F by the Second Incompleteness Theorem. And if the machine has n states, then the value of BB(n) is unprovable in F.
If F=ZFC, then the current record (improving on my and Yedidia’s initial result of ~8000) is a 745-state machine whose behavior is provably independent of ZFC. Obviously there’s still a large gap between 5 and 745, and I think narrowing that gap is a wonderful problem.
Note however that this is all relative to a theory. E.g. just because some machine’s behavior is independent of ZFC, doesn’t mean it couldn’t be proved to run forever by a more powerful theory.
Comment #50 July 3rd, 2024 at 5:09 pm
That’s amazing, I’m going to read the paper, thanks
Comment #51 July 3rd, 2024 at 5:21 pm
helicopterosaur #48: Check out Section 5.6 of my survey, which is about exactly that question!
Comment #52 July 4th, 2024 at 1:25 am
I too enjoyed one of A.K. Dewdney’s compilations of computer recreations, The Armchair Universe, as an adolescent who was learning how to program. I bet he inspired a lot of young nerds in the ’90s, so I’m quite disappointed to hear that he became a 9/11 truther.
Comment #53 July 4th, 2024 at 4:13 am
Scott #42:
As big math fan (but a physicist), I’m not trying to reduce everything to useful to physics or not. I’m perfectly fine with “unuseful” math. Still, I was just trying to better understand the hypotheses behind certain statements (infinite sets/tapes as we discussed, for example) and the possible implications for physics (if there aren’t, it remains great stuff).
Your comment about emergence of complexity from simple rules reminds me of Wolfram’s ideas.
Thanks again for the answer and thanks for blogging this BB(5) great news.
Comment #54 July 4th, 2024 at 6:49 am
So now we know that the first five Busy Beaver Numbers ARE computable. Is the question “what is the largest computable Busy Beaver Number?” a computable question?
John K Clark
Comment #55 July 4th, 2024 at 6:52 am
I should also note that I’ve asked a related graph theory question on Mathoverflow https://mathoverflow.net/questions/474458/are-directed-graphs-with-out-degree-exactly-2-strongly-connected-with-probabilit . The question is inspired by Busy Beaver and the motivation is explained there, but the question itself is purely a question about the properties of random graphs.
Comment #56 July 4th, 2024 at 7:30 am
John K Clark #54: The concept of “computability” applies only to infinite sequences and functions, not to specific integers. (Or if you like, every specific integer is “computable,” in that there exists a program to output that integer!)
What you can ask about, is how many values of the BB function are determined by some particular axiomatic system like ZF set theory. We now know that the answer is at least 5 and at most 745. I’d guess that the truth is much closer to the former. And no, the answer doesn’t itself need to be provable in ZF theory (but it might be—we don’t know!). For more, see my comment #49 in answer to Random.
Comment #57 July 4th, 2024 at 10:31 am
FYI (unmentioned in your post so apologies if this isn’t news) A. K. Dewdney also passed away in March of this year.
Comment #58 July 4th, 2024 at 10:46 am
Eric Taylor #57: I’m sorry to hear that. Like I said, his book had a huge and positive impact on me.
Comment #59 July 4th, 2024 at 11:59 am
@scott #10 – yes, was going to say the thing about Coq – if that encourages its use among other mathematicians, or pushes more research into similar systems, then that’s a huge impact in itself
Comment #60 July 4th, 2024 at 12:07 pm
Pete #59: The more I think about it, the more I suspect that’s the biggest real-world impact that this is likely to have. A famous open problem in math and computer science was finally solved, and it probably could not have been done in practice without formal verification software. That’s a major milestone for the field of formal verification itself, unless I’m mistaken. On Twitter, Talia Ringer asks whether I’ll concede this, and the answer is yes.
Comment #61 July 4th, 2024 at 12:14 pm
@Anon #10
What I actually meant is that none of it is frivolous in my opinion – just as art and music are not frivolous. But I think you’d find very few theoretical mathematicians who would say they study it because of the practical application.
Comment #62 July 4th, 2024 at 1:10 pm
Now that the claim is known to be provable somehow, what is the weakest system that proves it? I don’t think it uses any infinitary reasoning, so at most PA. I am aware of two non-trivial proof techniques involved:
1. Some of the “filters” use something like regular expressions to identify repeating tape patterns.
2. Fibonacci reasoning involving Zeckendorf’s theorem (https://www.sligocki.com/2023/03/14/skelet-10.html)
Are these required for any proof, or is there a simpler proof not involving them? If they are required, is the weakest system that proves them?
Comment #63 July 4th, 2024 at 1:15 pm
Nick Drozd #62: Wonderful question!! I have no idea. But it occurs to me that the entire proof already being formalized in Coq provides a perfect starting point for someone potentially to answer that question soon, if they want to.
Comment #64 July 4th, 2024 at 2:28 pm
Scott #49,
“Note however that this is all relative to a theory.”
I think Random in #47 may have been asking if there exists a Turing machine whose non-halting behavior cannot be proved under any theory no matter how powerful? And then the follow-up whether this meta question can be resolved under any theory?
Turing machines that are outside of any theory…
Comment #65 July 4th, 2024 at 2:39 pm
Adam Treat #64:
I think Random in #47 may have been asking if there exists a Turing machine whose non-halting behavior cannot be proved under any theory no matter how powerful?
In that case, the answer is no. Given any TM that runs forever, you can always just add an axiom that says that that TM runs forever! (Or, eg, what’s the value of BB(n), for any n of your choice.) Reflect on this and you will better understand Gödel.
Comment #66 July 4th, 2024 at 2:56 pm
@Max #21:
Another model that AFAIK has interesting boundaries is 1d cellular automata. Rule 110 is universal on a repeating background but I don’t think any neighborhood-1 rules are know that are universal on a blank tape. (And the universality of rule 110 seems to have more or less stopped research into the question, which is IMHO a shame).
Comment #67 July 4th, 2024 at 11:40 pm
Random #47, Scott #49:
Drive-by comment to point out that https://ar5iv.labs.arxiv.org/html/1605.04343 may be much more convenient for people with mild-to-moderate pdf allergies 🙂
Comment #68 July 4th, 2024 at 11:47 pm
Scott #49:
Would it be possible that a Turing machine that loops through all the theorems of F might also never halt if the order in which it tests theorems is such that it’ll never get to a contradiction?
That is, is it possible that there’s a BB(n ∈ ℤ) ∉ ℤ?
“The value of BB(n) depends on whether you consider halting after a countable infinity of steps legitimate”.
Comment #69 July 5th, 2024 at 6:37 am
Carey Underwood #68: In order to get the result I said, you specifically design the machine so that it eventually hits all the theorems (for example, by checking them in breadth first search order).
Comment #70 July 5th, 2024 at 8:55 am
In addition to Zermelo–Fraenkel and the Axiom Of Choice, in your opinion do you think someday we will be able to add another fundamental axiom that has the following properties:
1) It’s simple.
2) Intuitively it seems reasonable and true.
3) It does not introduce any new contradictions to existing mathematics.
4) It will allow us to prove and disprove interesting things that currently we cannot.
It seems to me that if it doesn’t meet all these specifications then we’re stuck with what we have now.
John K Clark
Comment #71 July 5th, 2024 at 9:07 am
John K Clark #70: There’s no limit to the plausible-looking and conceivably useful new axioms you can add … if nothing else, then Con(ZFC), Con(ZFC+Con(ZFC)), etc. 🙂
Having said that, it’s hard for me to imagine that PA and ZFC will ever lose their pride of place, but you should really ask a set theorist, not me.
Comment #72 July 5th, 2024 at 5:51 pm
John K Clark #70: Hugh Woodin’s highly conjectural axiom called “V = Ultimate L” comes to mind.
Dmytro Taranovsky seem to be a very serious amateur (much more serious than myself), when it comes to questions like your 1-4 (maybe except “4) It will allow us to prove and disprove interesting things that currently we cannot.”)
https://lists.ugent.be/wws/arc/fom/2024-04/msg00009.html
https://lists.ugent.be/wws/arc/fom/2024-04/msg00012.html (his latest FOM posting on related topics)
https://web.mit.edu/dmytro/www/main.htm
Comment #73 July 5th, 2024 at 5:56 pm
Isn’t BB(6) already proven weakly universal? If so, isn’t the busy beaver challenge technically over?
Comment #74 July 5th, 2024 at 6:03 pm
Alex Skryl #73: What would it even mean for a specific number like BB(6) to be “weakly universal”? And how could the challenge be over, when it clearly remains to find better lower bounds on BB(6), BB(7), and so on, and/or to prove that various difficult 6- and 7-state machines run forever?
Comment #75 July 5th, 2024 at 6:10 pm
John K Clark #70: There sure are such axioms: Large Cardinal Axioms. They are natural extensions of the idea of infinity. The idea is roughly “Every definable closure property of the universe should already reflect down onto a set and the universe itself is undefinably big.” Most set theorists regard Large Cardinal Axioms as obviously true. They are compatible and form a (mostly) nice hierarchy. So modern math is ZFC + some LCA (depending on use case) not just ZFC alone.
These axioms have interesting applications to classical math. For example take a supercompact cardinal (a large cadinal with convenient reflection properties). Then all sets of reals that are geometrically defined (so called projective sets) are Lebesgue measurable. You actually need the AC to Banach-Tarski decompose a ball (under V=L a projective decomposition exists). Even stronger: The principle of Projective Determinacy (PD) holds and the theory of the real line (equivalently the theory of P(N)) is effectively complete (apart from Gödel sentences). This is a result from the 1980s due to Martin, Steel and Woodin.
The philosophical implications are quite profound. As for number theory, there is no multiverse at the level of the reals (P(N)), also called “second order number theory”). Natural combinatorial questions about P(N) seem to have one and only one true answer and the answer can in principle be derived from PD.
With third order number theory and above it is unknown wether there is a universe or a multiverse. Combinatorial questions about P(P(N)), e.g. the Continuum Hypothesis (CH), might be meaningless. We know that Large Cardinal Axioms don’t fix CH and the like. But there is a research program by Hugh Woodin, a search for an “Ultimate-L” Axiom that we hope will yield a canonical Universe.
(Note that not every Set theorist agrees with this view, see David Joel Hamkins)
Comment #76 July 5th, 2024 at 6:15 pm
@Nick Drozd, #61
It was at least to me surprising how little it seemed one needed to resolve BB(5). My reaction after seeing that was to guess that ZFC is sufficient for determining BB(6) but that humanity will never manage it.
Comment #77 July 5th, 2024 at 6:18 pm
You write this:
>>The news these days feels apocalyptic to me—as if we’re living through, if not the last days of humanity, then surely the last days of liberal democracy on earth … At a terrifying time for the world, I’m happy that, whatever happens, at least I lived to see [the calculation of BB(5)].
In your previous post and comments there, you make it clear that this threat to democracy you imagine is Donald Trump, and one of the “news these days” is Biden’s poor debate performance.
I’m curious: How is Trump the one who’s a threat to democracy, when it’s the Democrats and Biden who weaponized the courts and the justice system to put their political opponent (Trump) in jail? Isn’t that classic autocrat behavior?
Comment #78 July 5th, 2024 at 6:20 pm
@Scott #71,
It seems likely that there will be many statements that undecidable in ZFC for reasons which have nothing to do with consistency of ZFC. The same likely applies to other system It seems (at least to me) likely that whatever the highest BB value one can determine in ZFC, it will be the same for value for ZFC+Con(ZFC). And I’d make the same guess for PA.
On the other hand, ZFC+Con(ZFC) is in some sense morally very close to ZFC + there is a large cardinal. And it does seem that really strong versions of large cardinal axioms might resolve enough things to be able to pin down BB values. (But I’m also somewhat skeptical of the consistency of a lot of the more extreme large cardinal axioms.)
Comment #79 July 5th, 2024 at 7:38 pm
Off topic but a wtf:
https://www.newscientist.com/article/2436023-multiple-nations-enact-mysterious-export-controls-on-quantum-computers/
Comment #80 July 5th, 2024 at 8:11 pm
Adam #77: Your comment, which you’ve submitted multiple times, reminds me of the smirking bully who says “stop punching yourself!” You know perfectly well that Trump is the one who shattered all the norms of liberal democracy—withholding arms to Ukraine unless Zelensky helped his campaign, paying hush money to a porn star, etc etc and then finally egging on an insurrection that came very close to reversing an election for the first time in American history. You know that the multiple investigations and trials have been a feeble and, so far, totally ineffectual attempt to hold the traitor accountable. You enjoy pretending that you don’t know these things, and that Biden is actually the one to blame (!). I won’t continue to humor your enjoyment. All further comments about this will go straight to the garbage. Unlike with the anti-Israel and social justice people who constantly attack me from the other side, I don’t even respect your position enough to be goaded into back-and-forth exchanges about it.
Comment #81 July 5th, 2024 at 10:59 pm
Adam #77
“when it’s the Democrats and Biden who weaponized the courts and the justice system to put their political opponent (Trump) in jail? Isn’t that classic autocrat behavior?”
Trump was found guilty by a jury in his sexual assault civil case trial and in the hush payment case. Juries aren’t “part of the courts”, this is actually in line with a democratic system, juries aren’t bought and both defendant and accuser have to agree when picking them.
If the justice system should be dismissed just because they found your superstar guilty, that’s the “classic autocrat behavior”.
Also, in all the other pending cases, Trump has actually appointed the judges (including the supreme court recent decision), and they’re clearly giving him huge breaks.
So, there’s “balance”, Biden isn’t “in control” of the justice system.
That’s just like all the “stop the steal” bullshit, acting as if massive election fraud is an actual thing, and then by some miracle only the democrats would be doing it, the MAGA side is just too righteous to pull it off… what a f’ing joke.
Anyway stop acting as if any of this matters to people like you… as Trump put it 8 years ago:
“I could stand in the middle of Fifth Avenue and shoot somebody, and I wouldn’t lose any voters, OK? It’s, like, incredible.”
Comment #82 July 6th, 2024 at 4:26 am
I believe I first read about BB circa 1980 in scientific American (SA). But then there was another SA event which eventually involved BB
They had an article about social games like repeated prisoner’s dillema competition and how tit-for-tat and other “nice” strategies did well
Then they offered a potential 1,000,000$ award. Each participating reader will send SA a postcard in which they will write a number. The winner was the person who wrote the largest number and the prize was 1,000 000 divided by that number. The collective winning strategy was for each potential participant to choose to actually send a number with a very small probability and to write a very small number, 1 or 2
Instead it turned out into a who can write the largest number on a postcard competition, with the naive crowd writing writing many 9s, then those iterating exponents and finally those iterating BB.
Comment #83 July 6th, 2024 at 9:44 am
Joshua Zelinsky #78: There’s no reason to expect BB(n) to align nicely with Gödel consistency strength. Strong axioms might well be definable with less symbols than weaker ones. It’s shorter to state “a nontrivial elementary embedding from V into V” than “a nontrivial elementary embedding from V into M with complicated closure properties about M”. And “0=1” is quite short :-). The smallest Turing machine that halts iff ZF is inconsistent might very well be larger than the smallest TM that halts iff T is inconsistent for some (not known to be inconsistent) theory T stronger than “ZF+Reinhardt Cardinal”.
Now, BB(n) talks about _all_ algorithms that can be implemented on a n-state TM (with 2 tape symbols, …). But is this useful? What does that even mean, what do these algorithms have in common? Why should we group them together in this particular way in the first place? Can we even say anything reasonable about them unless n is very small? Probably not.
IMHO the BB function is an ill motivated concept. It depends on a very specific model of computation that just happens to be popular for historical reasons. Use different computer models and measures of “size” of these models, then algorithms will get partitioned in quite different (but equally meaningless) ways. My gut feeling is that the first n for which there is no proof of the value of BB(n) in PA, the strongest known Set Theory axioms still fail to do the job. (Of course we will never know this for sure because that kind of question is intractable by design.)
Comment #84 July 6th, 2024 at 10:14 am
Gerald #83: Obviously you have to make some arbitrary choice of programming language (just like with Kolmogorov complexity and other concepts of computability theory). In my survey, I discuss the motivation for choosing Turing machines—besides the historical one, it’s also that you get complicated, unpredictable behavior already with 3 or 4 instructions, without in any way rigging to rules in order to get it.
As I also say in the survey, I love the question of whether there’s a gap between the n at which the value of BB(n) first becomes independent of ZF, and the n at which the value of BB(n) first implies Con(ZF). I hope someday we do learn the answer to that question—but that would require, at minimum, the development of new techniques for proving independence from ZF.
Comment #85 July 6th, 2024 at 11:11 am
This is exciting news and congrats to everyone involved! Glad that A.I. couldn’t beat us to the punch.
Whenever undecidability, ZFC, or uncountability come up, I can’t help but wonder why we can’t build a new foundations for mathematics where we clearly delineate undecidable or uncountable objects as off limits and remain within the scope of countable set theory (which typically takes ~30 mins in Data Structures to explain). Isn’t the beauty of uncomputability (like Cantor’s original proof) that we can say certain objects are beyond reasonable discussion (like BB(n) for the sequence, with finite n being really interesting, or a real value where you don’t know which real value you want)?
Its a dirty little secret that we don’t need the reals for calculus or to write code to approximate sqrt(2) or pi. Isn’t it time we build all parts of legitimate mathematics, including calculus, on the foundation of computable functions and countable sets? At least so we don’t waste decades on metaphysical questions about uncountably infinite sets and getting jackhammered by paradox after paradox?
Comment #86 July 6th, 2024 at 2:21 pm
Avocado #85: It’s a hell of a lot harder than you suggest to draw a clean line separating the mathematical questions we’re allowed to ask from those we aren’t. Like, are we allowed to define BB(6), but not BB(7)? Who gets to decide, you?
Also: if uncomputable problems are off-limits, can we at least raise the question of whether a problem (like solving polynomial equations over the rational numbers) is decidable or not, and ban it from discussion only if it ends up being undecidable? 🙂
Whether in the foundations of quantum mechanics, here, or anywhere else, I feel like philosophies of “you’re not allowed to ask about such-and-such” have a poor track record, unless they give us a new understanding reality that shows why the forbidden question is meaningless.
Having said that, there’s a milder version of this that I endorse. As I said earlier, I’m a Platonist about arithmetical questions like the Goldbach Conjecture. But as a question becomes harder and harder to express by quantification over integers and finitary computations, I become less and less Platonist and more and more formalist about it.
Comment #87 July 6th, 2024 at 2:25 pm
In response to Adam in Comment #77
Now that 6 Justices of the Supreme Court, 3 that Trump appointed and 3 that other Republicans appointed, have decreed that a president staging a coup d’état is part of his “official duties” and thus perfectly legal, and given the fact that being the Commander in Chief is also part of a president’s official duties, if I could ask Donald Trump one question it would be this: “Do you believe it would be within Joe Biden’s rights if right now, this very moment, he ordered Seal Team Six to shoot you in the head?”
I don’t know how Trump would answer that question, but I know what Justice Sonia Sotomayor, who incidentally was NOT appointed by trump or any other Republican, said in her dissenting opinion:
“The long-term consequences of today’s decision are stark. The Court effectively creates a law-free zone around the President, upsetting the status quo that has existed since the Founding. The President of the United States is the most powerful person in the country, and possibly the world. When he uses his official powers in any way, under the majority’s reasoning, he now will be insulated from criminal prosecution.”
“Orders the Navy’s Seal Team 6 to assassinate a political rival? Immune.
Organizes a military coup to hold onto power? Immune.
Takes a bribe in exchange for a pardon? Immune. Immune, immune, immune.
Let the President violate the law, let him exploit the trappings of his office for personal gain, let him use his official power for evil ends. Because if he knew that he may one day face liability for breaking the law, he might not be as bold and fearless as we would like him to be. That is the majority’s message today.”
John K Clark
Comment #88 July 6th, 2024 at 2:38 pm
Gerald #83
This would be an interesting scenario. I think a lot of people imagine that there is some rich structure connecting BB numbers to consistency strength, where say BB(6) is equivalent to PA, then BB(7) is equivalent to ZF, some number corresponds to some large cardinal, something like that. But with what you’re proposing, it goes provable, provable, provable, then BAM, all the unprovability shows up all at once, and there are no human-practical rungs to the ladder.
It’s not so implausible. All it takes is that for some N, PA can prove BB(N) and ZF (etc) can’t prove BB(N+1). Why not? Experience shows that the explosive growth of BB is more explosive than anyone ever expects, so why shouldn’t it explode right past PA-unprovability?
Comment #89 July 6th, 2024 at 2:53 pm
By the way, here are the latest results for the Beeping Busy Beaver problem, the super-uncomputable variation of BB:
Comment #90 July 6th, 2024 at 3:24 pm
Scott #86: “It’s a hell of a lot harder than you suggest to draw a clean line separating the mathematical questions we’re allowed to ask from those we aren’t. Like, are we allowed to define BB(6), but not BB(7)? Who gets to decide, you?”
Is it so hard? If its undecidable or unrecognizable, then we know what that means. From my understanding BB(6), BB(7), or for any specified n is not proven to be undecidable is it? Or did I misunderstand your comment #56?
I think what’s wrong is that you show people something if uncomputable, like Cantor did, and then claim this is a really important step (closure of the reals) to prove a bunch of wonderful things in analysis. Turns out, computable analysis and calculus exist and we don’t the reals for anything, we just need computable functions (duh). I guess you could claim its a nice short cut for some proofs, but then why waste so much time debating concepts like the Axiom of Choice or other notions that are superfluous to the countable case.
Still, it feels many practitioners in advanced mathematics and even logic lack a grasp of what a result like undecidability means for the concept they are trying to study. Its a massive chasm and you should wander into topics associated with it with great care. Like dedicating your life studying models in model theory that become trivial (or trivially alike) over countable sets. Or working hard to define notions like measurable that look trivial over countable sets.
Comment #91 July 6th, 2024 at 3:51 pm
Gerald #83: One can least minimize the dependence on computational model by choosing an additively optimal one as we do in Algorithmic Information Theory. See comment #46.
Comment #92 July 6th, 2024 at 4:10 pm
Avocado #90: The idea that one can talk about the “decidability” of a specific integer like BB(6) is a Zombie Misconception, one that keeps reappearing in this comment section no matter how many dozens of times I explain what’s wrong with it. At most you can ask whether the value of BB(6) (say) is provable within a given axiom system, like ZFC. Every BB value is provable in some axiom system.
It’s true that transfinite set theory has few or no direct applications, but then again, neither do algebraic geometry or 5-dimensional topology! And if you allow indirect applications, the concepts of diagonalization, forcing, etc have been crucial in theoretical computer science, including for more “down-to-earth” questions.
Comment #93 July 6th, 2024 at 4:40 pm
Avocado #85: On the one hand, Norman Wildberger tries to do what you are suggesting:
https://web.maths.unsw.edu.au/~norman/views.htm
https://www.youtube.com/@njwildberger/videos
On the other hand, I would be careful with people who criticize everybody else. They might be perfectionists with impossible standards, or stubborn and refuse to change their mind. If he raises some problem in one of his videos, do you believe that anybody (especially any of his normal students) would have a chance to convince him that this problem has been solved? See
https://gentzen.wordpress.com/2019/04/16/theory-and-practice-of-signed-digit-representations/#RedundantRepReals
What type of answer would you expect from Norman Wildberger? Perhaps
Or simply silence? To not be too unfair, let me reveal that much: The answer wasn’t complete silence, but it wasn’t “Oh, I see, somebody really solved this problem” either.
Compare this to people like Scott, who gave a task to his student Ewin Tang to show that a classical computer couldn’t solve a certain problem efficiently, and who could be convinced by her that a classical computer actually could solve it efficiently.
Comment #94 July 6th, 2024 at 9:38 pm
Scott #92: I agree, but don’t totally follow. How about BB(6), BB(7), BB(8), etc. is there an algorithm that can find that value? I mean on a real machine like BB(5) was. I don’t understand why I should care about an axiom system at all. Do we need to define anything beyond the 7-tuple Turing machine? We can simulate that on real machines right? Are you sneaking computational power into the axioms?
In terms of algebraic geometry or 5-dimensional topology, I also don’t follow. Those do, in my view, have bearing on reality and I think we can state every important statement about them using computable values. If we want to use a value from any branch of mathematics to do something with it, we will have to compute that value (or an approximation of it).
Gentzen #93: I feel like there is fork in the road for the question: you have to keep error bounds around if you really want that value or you have to accept the utilization of a symbolic system where that real value becomes part of your alphabet. Then in the end you can say you know there is an algorithm that can get whatever bound you need on that value and you really do have those infinite choices in libraries to compute it as mathematicians like. And we can have improvements, like Leibniz, Ramanujan, etc. for computing them. I can understand that certain statements in analysis, if we really track all the error bounds, may become more cumbersome (and honest). There is probably a lot of really wonderful complexity statements to be hunted in different branches of mathematics that we’re actually missing. In terms of reducing redundancy, that seems like an interesting algorithmic problem, like tokenization in LLMs or lossless data compression.
“But even with an algorithmic orientation, you first have to establish a theory of “algorithms”–not within computer science, but as part of pure mathematics. This is a huge endeavour. I don’t think anyone has come anywhere near close to resolving it.”
This feels wrong, because we should start with the nuts and bolts that work well and intuitively (actual algorithms like in Art of Computer Programming) and then try to develop something that works for most of the important stuff we actually care about (that’s all in plain sight for modern programming). Then we can worry about the edge cases, which I would guess are mostly pathological or extremely valuable to investigate. I’d even be happy to start with finite automata before going to Turing machines. Either way, we come out ahead doing this stuff the right way. Maybe we’ll never satisfy Wildberger to the infinite degree but its already good enough to power the entire world’s economy that runs with actual computers from the get-go.
I can’t think of anything important we’ve gotten from transfinite sets, but I don’t think anyone can argue about, for example, the value of Arnoldi’s method. If we did get something, I would guarantee it’s translatable to countable sets and computable functions. Know of anything of value that isn’t??
Comment #95 July 7th, 2024 at 3:24 am
Avocado #94: The fundamental error you keep making is to ask whether there is or isn’t an algorithm to compute a specific number like BB(6). Formally, that’s a nonsense question. Of course there’s an algorithm! Namely, for whichever integer k happens to equal BB(6), “print k.” The point is that the whole concept of computability applies to functions mapping integers to integers, and does not apply to specific integers. For any specific BB value, there’s nothing that proves we can never know its value, unless you identify “knowing” the value with proving it in some specific axiom system like ZFC. To learn BB(6), you “merely” need to solve all the math problems involved in determining whether 6-state Turing machines halt—a finite list of problems, each of which presumably has a solution if your axioms are powerful enough (the remaining question is how powerful they need to be).
At this point, however, I’ve exhausted all possible ways I know how to explain this and I give up — maybe someone else wants to try.
Comment #96 July 7th, 2024 at 6:33 am
Avocado Says in comment #94
> I don’t understand why I should care about an axiom system at all
If you care about proofs then you should care about axiom systems because you can’t prove anything without an axiom system. Suppose using nothing but the axioms in ZFC you constructed Goldbach’s Conjecture, or to put it another way, you proved Goldbach’s Conjecture: it would still be conceivable that a huge computer might someday find an enormous even number that was not the sum of two prime numbers, but if that very unlikely event were too happen it would create the largest crisis in the history of mathematics because it would mean that ZFC is inconsistent. Proving X does not necessarily mean that X is true because an axiom system is only as strong as its weakest axiom. That’s why you need to be super conservative before you start adding new fundamental axioms.
John K Clark
Comment #97 July 7th, 2024 at 8:56 am
Scott #86,
The most difficult “not allowed to ask” question to grasp for the people has been the one popularized by Stephen Hawking. He famously dismissed the question of what happened before the Big Bang by saying it is not a question allowed to be asked because Time itself did not exist before the big bang ? This one looks like the mother of all those not allowed questions because everyone can intuitively understand time but not the fact that is has a beginning.
Comment #98 July 7th, 2024 at 9:42 am
Prasanna #97: It’s not so much that Hawking said you’re not allowed to ask, as that he had a specific proposal (the “Hartle-Hawking No Boundary Proposal”) where the Big Bang is a smooth cap rather than a singularity, so that (as he loved to put it) “asking what came before the Big Bang would be like asking what’s north of the North Pole.” Hawking held philosophy in low regard and was not always philosophically careful. I would say in any case that, even if we knew there was nothing “before” the Big Bang — even if the Big Bang was the earliest you could go in time — the causal question of why the whole spacetime manifold came into existence at all would barely have been touched.
Comment #99 July 7th, 2024 at 11:15 am
Avocado #94: “I can’t think of anything important we’ve gotten from transfinite sets”
The TREE function originating from Graph Theory is computable (Remember: TREE(3) is a famous example for a big natural number). Yet it’s existence cannot be proved by finitistic methods. It’s not doable in PA. The proof that the TREE-algorithm terminates for every input argument requires transfinite ordinals.
So, even if you are only interested in computable things you need transfinite math. The infinite world tells us something about the finite world. (And larger infinities tell us something about smaller infinities.) You may want to watch a talk about “Necessity of the Infinite” by Hugh Woodin on Youtube.
Comment #100 July 7th, 2024 at 12:46 pm
John K Clark #96: Not true, if we want a computer system to provide a proof then we need to formalize the axioms and they would be about the formal manipulation of the Turing machine. Does PDL need ZFC?
Scott #95:
”
To learn BB(6), you “merely” need to solve all the math problems involved in determining whether 6-state Turing machines halt—a finite list of problems, each of which presumably has a solution if your axioms are powerful enough (the remaining question is how powerful they need to be).
”
How much would you wager that the Axiom of Choice needs to be utilized to prove the hold-out Turing machines do (not) halt for BB(6) (or BB(n) for any finite n)?
Comment #101 July 7th, 2024 at 1:12 pm
Avocado #100:
How much would you wager that the Axiom of Choice needs to be utilized to prove the hold-out Turing machines do (not) halt for BB(6) (or BB(n) for any finite n)?
It’s known that the Axiom of Choice is never needed for arithmetical questions, like determining BB(n) values! It’s a very special case of something called the Shoenfeld absoluteness theorem.
Having said that, yes, we know that some set-theoretic principles beyond ZF will start being needed to determine BB(n), at some n from 6 to 745. I strongly conjecture that it happens closer to the lower end of that range.
Comment #102 July 7th, 2024 at 2:52 pm
Scott 101, the argument is incorrect because the Busy Beaver function, BB(n), involves non-arithmetical questions about Turing machine behavior, which can require set-theoretic principles beyond ZF, beyond the Shoenfeld absoluteness theorem’s scope.
Comment #103 July 7th, 2024 at 4:34 pm
Stammanis #102: Nope. Questions of the form “does this Turing machine halt?” are always arithmetical (Σ1 in particular).
Comment #104 July 8th, 2024 at 2:25 am
I wonder can we find the minimal proof-theoretic ordinal among theories that prove the value of BB(5)? Is it actually a correct (and reasonable) question to consider?
Comment #105 July 8th, 2024 at 5:45 am
Danylo Yakymenko #104: Yes, that (or more broadly, the question “what is the weakest proof system that proves the value of BB(5)?”) is an excellent question, and I think the most important thing to have emerged from this comment thread. I already emailed Tristan Stérin to suggest that the bbchallenge collaboration look into it. (Then again, since their code is public, anyone else could as well!)
Comment #106 July 8th, 2024 at 7:27 am
Avocado Says in Comment #100
> ” if we want a computer system to provide a proof then we need to formalize the axioms and they would be about the formal manipulation of the Turing machine.”
If nobody trusts that all the axioms in your formal system are correct then nobody will believe that any of the proofs you obtain from that system will tell them anything about the real world that is true. Kurt Godel showed us that no axiomatic system can be both consistent and complete, and also that no axiomatic system can prove its own consistency. Mathematicians don’t like it but they can live with a system that is not complete, but one that is not consistent would be catastrophic. Obviously nobody can prove it but most mathematicians think ZF is consistent, thus they are very reluctant to start screwing around with it. That’s why I think saying ZF can never determine the value of BB(746) is *almost* the same as saying BB(746) is not computable, adding an additional axiom to ZF will never be universally accepted as a good idea.
John K Clark
Comment #107 July 8th, 2024 at 7:31 am
John K Clark #106: There is a well-known way to add axioms to ZF, that should be universally accepted by anyone who accepts ZF. That’s to add Con(ZF), Con(ZF+Con(ZF)), etc., ultimately proceeding through the computable ordinals. But then the question shifts to the largest n such that BB(n) can be determined by ZF plus a chain of consistency statements indexed by an ordinal notation that “we all agree is reasonable.”
Comment #108 July 8th, 2024 at 7:39 am
Hi Scott,
I went back to read your and Yedidia’s paper and on page 7 you mention that you can calculate the bits of complexity of ZF and in general it is possible to calculate how many bits of complexity a mathematical statement has (citing Calude and Calude).
This got me wondering, about how this relates (if it relates at all) with the maximum amount of information you can store in the universe (for instance discussed here but I’m sure you are aware of the argument).
The question would be: how much complexity in terms of mathematical statements can the universe contain? Having an upperbound has any consequence or I am just comparing apples to oranges?
Comment #109 July 8th, 2024 at 8:13 am
Scott #98,
Its just not the spacetime manifold, but the whole known universe, that is energy/matter that came into existence at Big Bang ? Since all “physical” entities exist only after the Big Bang, any causal explanation should involve either metaphysical, or no such explanation make sense, or its unknowable ?
Comment #110 July 8th, 2024 at 8:31 am
Scott #74: What I meant to say was that the 6-state, 2 symbol Turing machine was proven weakly universal. So with BB(6) relying on this type of machine, how can there be an upper bound on the output length if we can’t know if it ever halts? Looking back at the BB requirements, it seems like the tape must start out blank, so weak universality which requires a particular starting state doesn’t seem to apply, which makes the machine decidable. Is that the right way to think about this? Does the BB challenge essentially end once you reach a fully universal TM size? (proven universal with a blank tape)
Comment #111 July 8th, 2024 at 9:19 am
Alfio #108:
The question would be: how much complexity in terms of mathematical statements can the universe contain?
Not sure I understand the question. The Bekenstein bound together with the cosmological constant (if it’s indeed constant) imply an upper bound of ~10122 on the number of bits or qubits that can be stored in the observable universe. You could then (in principle!) use those bits or qubits to represent mathematical statements in any way you wanted, with I suppose the main other constraint being how much computation you can do between now and the heat death of the universe.
Comment #112 July 8th, 2024 at 9:20 am
Alex Skryl #110: For the Busy Beaver game, the concept of universality is not directly relevant, because we only care about what each machine does on the all-0 initial state.
Comment #113 July 8th, 2024 at 9:22 am
Hi, Scott ; there is still something I don’t understand in the sentence « calculate BB(n) » (or even give a lower bound) . If, for instance, there exists a TM of 20 states calculating TREE(100), this gives obviously a lower bound for BB(20), but what does it mean ? This number is not only unknowable (and its existence not provable in PA or much stronger systems in substantially less than this number of steps), but there is no way to express it in a more intuitive system, like the fast growing hierarchy. So it is not more useful to give a bound to BB(n) that to simply give the definition of. BB(n), or I am missing something ?
Comment #114 July 8th, 2024 at 10:05 am
f3et #113: The task can be operationalized as, “give a program that computes BB(20) (or whichever value we’re talking about) and then halts, together with a proof of the program’s correctness.”
Comment #115 July 8th, 2024 at 11:41 am
This is great news! Hearing the news made me interested in busy beavers again.
In 2014, I wrote a blog post proving a lower bound for BB(7). After hearing the news, I have read many web pages about BB, and I was pleasantly surprised to discover that my blog post has been cited in multiple places, and the idea from the post has been used to calculate the current lower bound for BB(6).
Looking forward to what the collaboration will discover next!
Comment #116 July 8th, 2024 at 12:53 pm
Avocado #85
Your comment refers to both undecidability and uncountability. These are related concepts, but they are not the same thing. In particular, the definition of the Busy Beaver function makes absolutely no reference whatsoever to anything that is even countably infinite, much less uncountable.
There are only finitely many programs of a given length. Finitely many of these programs halt. Every program that halts does so within a finite number of steps. Every finite set of numbers has a maximum, and that maximum is the Busy Beaver number for the given program length.
Notice too that if a program actually does halt, its haltingness is trivially provable (trivial in theory, that is). Thus for every N, it is trivially provable that BB(N) ≥ M, where M is the actual value of BB(N). The tricky part is “just” in proving that that lower bound is tight.
Comment #117 July 8th, 2024 at 1:43 pm
Isn’t it possible that for every BB(N) the winning Turing machine happens to encode something similar to the one for BB(5)? I.e. some variation of the Collatz conjecture function.
Comment #118 July 8th, 2024 at 3:07 pm
[…] The Blog of Scott Aaronson If you take nothing else from this blog: quantum computers won't solve hard problems instantly by just trying all solutions in parallel. « BusyBeaver(5) is now known to be 47,176,870 […]
Comment #119 July 8th, 2024 at 4:21 pm
UPDATE: Recall the phenomenal question posed in this thread, of what’s the minimal set of axioms needed to prove the value of BB(5). I passed this question along to Tristan Stérin of bbchallenge, who posted it on the Discord channel. mxdys (who played a central role in the Coq formalization) replied as follows:
halt, FAR and WFAR proof can be translated into (a subset of) PA, so all deciders we need for Coq-BB5 can be translated into PA for each decided TM.
for each TM with FAR/WFA cert, the closed set of reachable configs can be written as a predicate in PA, and by induction in PA you can show reachable configs are always in the set. there are a lot of details to show this.
And then a further update:
I believe BB(5) is in RCA0
So, modulo checking the details, it sounds like a small fragment of Peano Arithmetic should indeed prove the value of BB(5)…!
Comment #120 July 9th, 2024 at 12:40 am
Nick #116:
“These are related concepts, but they are not the same thing.”
Same proof, same beast. And that should make you queasy about uncountable sets being used nilly-willy everywhere.
“Every program that halts does so within a finite number of steps. Every finite set of numbers has a maximum, and that maximum is the Busy Beaver number for the given program length.”
Yes.
“The tricky part is “just” in proving that that lower bound is tight.”
Yes.
Scott #107: Care to say how you see these added axioms being useful? Of course if you add more axioms you’ll have more to compile for the consistency checking Turing machine which pushes up your best known upper bound for when you see the issue, but maybe not when it becomes a problem at all. I agree it’s likely to get worse closer to BB(7) than BB(500).
John K Clark #106:
“If nobody trusts that all the axioms in your formal system are correct then nobody will believe that any of the proofs you obtain from that system will tell them anything about the real world that is true.”
Where does set theory come into this? What about modal (dynamic) logic?
“Kurt Godel showed us that no axiomatic system can be both consistent and complete, and also that no axiomatic system can prove its own consistency. ”
Yes.
“they are very reluctant to start screwing around with it.”
Unfortunately, yes.
Gerald #99:
I only found some plain html which starts with a correction and talks about 2^(1000) symbols? I honestly don’t know, but if you say it I’ll believe you: yes or no, do we need uncountable sets to prove that there is a finite state Turing machine that uses some bounded number of tape to compute a finite value associated with a computable function (which apparently TREE is)? Or is this about countable ordinals that are all isomorphic to N?
In the end, I believe the Church-Turing thesis and to me that means we can only prove valuable things (as mere mortals) about the computable and the countable.
Comment #121 July 10th, 2024 at 3:37 pm
I have not seen mention in this thread of uncomputable numbers (outside integers). I see some potential on them to help dispel the zombies. Like comparing the integer BB(100) with the non-integers 1/BB(100) or sqrt(B(100)) and Chaitin’s constant.
And some unrelated questions. Since BB(n) is uncomputable for growing too fast I wonder: it is BB(n) mod 2 computable? And a connected question, let f(n) be the time to halt among Turing machines of n states that halt within an even number of steps. If f(n) computable?
And if you allow me to cast some little necromancy, consider “Is the smallest odd perfect number computable?”
Comment #122 July 10th, 2024 at 4:29 pm
Cristóbal Camarero #121:
– 1/BB(100), like any other rational number, is computable as a real number. If you want an uncomputable real related to BB, you can consider 1/BB(1)+1/BB(2)+1/BB(3)+… (I gave this as a homework problem in Quantum Computing Since Democritus!)
– The question about whether BB(n) mod 2 is computable is a favorite of mine! It was first raised to my knowledge by my former student Andy Drucker. I gave it a prominent place in my BB survey.
– The smallest odd perfect number probably doesn’t exist. But if it does, it’s as computable as any other fixed integer. 🙂
Comment #123 July 11th, 2024 at 10:14 am
Thank you Scott #122, I really should have read your survey before!
I have been pondering something related for some time, yet only in a shallow manner: can a quantum computer help on problems about the space of algorithms/Turing machines? Quantum computers seem to be useful to address problems with little data, like building a circuit to find factor of some number n. Indeed, this is a way to compute some constant. Quantum computers are said to relay on structure, like that of Abelian groups. The space of algorithms has structure, even if it is not trivial. I guess we would need to have some analogue of Fourier transform for collections of Turing machines. It would also make sense that we would have to resolve the P=NP question before being able to use quantum computers for these matters. Also, since BB grows so fast, it means that few states are necessary for complex behaviour, so few qubits could be sufficient for the part of selecting a Turing machine.
For the particular case of computing Busy Beavers, my gut guess is they will be as useless as classical brute force. I would expect some utility for analyzing machines with polynomial time. For example, could be possible to build a quantum circuit that outputs an algorithm to solve Orthogonal Vector Problem in O(n^k) for some given k?
Do you know if someone is studying this kind of thing. Or it is just dumb, and I am speaking from ignorance.
And another less related question, that I even though of emailing at some point but considered you would surely had better things to do: can quantum computers compute digits from number like pi or the gamma function faster than classical? For their relation with integer factorization it would make sense to me that the n-th digit could be computed using a quantum computer in O(log n) but to require O(n) when using a classical one.
Comment #124 July 11th, 2024 at 11:01 am
Cristóbal Camarero #123: No, I don’t see any obvious quantum speedup for computations related to Busy Beaver or the digits of pi or the gamma function. There’s always the Grover speedup, but not only is it modest, it doesn’t obviously address the bottlenecks for any of those problems…
Comment #125 July 22nd, 2024 at 7:48 am
[…] Quanta Magazine, 02 Jul 2024; Scott Aaronson, «BusyBeaver(5) is now known to be 47,176,870,» Shtetl-Optimized, 02 Jul 2024. En este blog también puedes leer «La función castor afanoso cumple 60 años», LCMF, 14 may […]
Comment #126 July 24th, 2024 at 1:43 am
Wow, that’s interesting!! I see the news only now…
As a querist follower, I saw the crpytids group on the bbchallange site.
I wonder if we have the opposite group “encryptids” for known theorems which can be translated to a turing machine with a low number of states.
The proof of the theorems is equivalent to the fact of machines halts/no halts so we might be able to create new deciders based on the general math knowledge (maybe it was done – I would be very glad for references).
If this is the case, maybe the Collatz conjecture could be solved not in the “regular” way of proofs but “easily” with new types of deciders from other results.
Comment #127 July 24th, 2024 at 11:13 am
Do we have an idea of what the busy beaver number that not only can’t be proved in ZFC but also can’t be proved in ZFC + statement that ZFC proves its own consistency and so on recursively (including transfinitely of course)? Also are there any other tricks to get more axiom that don’t cause problems?
Comment #128 July 24th, 2024 at 5:06 pm
Leo #127: Probably that could be done by modifying the existing constructions with ~750 states, adding a smaller number of extra states to encode the desired axioms like Con(ZFC). But the details would need to be checked.