> There are many variants of the original busy beaver problem, and some Busy Beaver Challenge contributors plan to keep working on these.
One such variant 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), 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.
A bit unrelated but you posted oeis so hoping you know.
In the article they mention there are 17 trillion possible 5-2 turing machines. I tried finding the sequence for this but couldn't.
Isn't there another formulation of BB where we count shifts (from left to right, and from right to left) a TM makes instead of strings of contiguous 1s. I remember seeing a video about this definition.
I worked for a couple years with a formidable and incomprehensibly smart engineer who ascended the IC ranks faster than anyone I’ve seen at an elite tech company. He quit the job a few years ago, and when I asked him his plans he told me he was going to work on the busy beaver problem. I can’t help but wonder if he is mxdys, the pseudonymous contributor mentioned in the article who wrapped up the formal proof of BB(5). I’ll probably never know.
One notable thing here is that the proof is a Coq proof. I wonder if it is the first significant proof that starts out implemented in a theorem prover, instead of being a known proof translated to such a system.
Note that there have been computer-assisted proofs before (four-color theorem, Kepler's conjecture), but those were not done in a formally verified setting until later.
Congratulations to the team! So the (blank tape) halting problem is solved for 5-state 2-color Turing machine programs. Has anyone tried applying these same techniques to the 2-state 4-color case? That seems like it would probably be tractable, although generally speaking colors are more powerful than states, so there might be some surprises there. (6-state 2-color and 2-state 5-color both seem intractable, perhaps even provably so.)
By the way, there is an extremely stupid but disturbingly widespread idea that humans are able to just intuit solutions to the halting problem, using the mind's eye or quantum mechanics in the brain or whatever. Needless to say, this did not factor into the proof.
Yes. In fact, Allen Brady feared as early as 1988 that there would be a totally intractable machine with 5 states [0]:
> Prediction 5. It will never be proved that Σ(5) = 1,915 and S(5) = 2,358,064. (Or, if any larger lower bounds are ever found, the new values may be substituted into the prediction.)
> Reason: 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.
Luckily, this prediction did not come to pass, but only by a margin of one extra state.
[0] Allen Brady, "The Busy Beaver Game and the Meaning of Life", in Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey, Oxford University Press, 1988, pp. 259–277. This chapter can also be found in the 2nd ed., Springer, 1995, pp. 237–254.
When you say "provably", do you mean that in the mathematical sense or in a practical sense?
For the practical sense, other commenters have already replied.
For the mathematical sense, I would say it would be pretty surprising to me if BB(5) had been undecidable -- 5 states and 2 symbols is just so few with which to try to encode undecidable behavior.
However, it's worth noting that as a consequence of the incompleteness theorem, there must be some n such that standard mathematics cannot prove the value of BB(n). And in recent years various people have been working on finding such n and seeing how low they can get the number. The current record[0] is 745.
I expect that record can be probably be brought lower (more easily than the record for computing BB can be brought higher!), but even so, that's a lot of distance between 5 (the highest we know) and 745 (the lowest we know to be unknowable).
[0]This is the current record both for ZFC and for PA, in case you're wondering what I mean by "standard mathematics"... so it at least ought to be possible to bring it down further for PA! I think so far nobody's found a way to do better for PA than for ZFC, even though, like, that has to be possible, right?
> But just four days ago, mxdys and another contributor known as Racheline discovered a barrier for BB(6) that seems insurmountable: a six-rule machine whose halting problem resembles a famously intractable math problem called the Collatz conjecture. Connections between Turing machines and the Collatz conjecture date back to a 1993 paper by the mathematician Pascal Michel, but the newly discovered machine, dubbed “Antihydra,” is the smallest one that appears unsolvable without a conceptual breakthrough in mathematics.
I wrote program to solve the cutting stock problem (https://en.wikipedia.org/wiki/Cutting_stock_problem) for a personal project. I couldn't (or didn't want to) use any existing program for it because my stock involved cutting pieces shaped like either /---/, /---|, or |---| and I didn't want to waste material on the 45 cut.
I find it interesting that the description of Brady's program to optimize search for BB(4) by cutting out search subtrees whose differences don't matter is fairly close to a description of what I did to make my program fast.
According to Scott Aaronson's blog post on this, there are 16,679,880,978,201 5-state Turing machines. I wonder if we know what percentage of them halt?
Edit: number of TM for n states: (4n + 1)^(2n). Found this (for smaller n), which is the kind of analysis I was curious about: https://github.com/LukasKalbertodt/beaver
All things considered, the proof is pretty short! It’s 19,000 lines of Coq (including white space and comments). And in my experience, if this were compiled into a traditional paper it would be significantly shorter than the Coq version. (Of course, length of the proof really isn’t a measure of difficulty or complexity, but it is a very rough yardstick we can use.)
When talking about the limits of human knowledge, I often think about the theorems that are provable, but so complex that no human being could understand them. Probably the most complex proof we have is the classification of finite simple groups, which is thousands upon thousands of pages, and there is probably very few or no people on Earth that fully understand all of it.
As the article suggests, BB(6) could be undecidable. But it could also have a proof millions of pages long, beyond the reach of humanity.
Maybe I’m just an unsophisticated code monkey, but I read a little about Busy Beaver from time to time and I just don’t get it. Why is this an interesting problem? What do we hope to learn from it?
IMO, because it gives you a way to know if a program will terminate or not. If it consists of 5 states and goes beyond 47176870 steps of execution, then it will never halt. However, we are currently limited to 1 to 5 states Turing programs. And you can make correspondance between some Turing machines and some theorems in Mathematics thus it gives you a way to prove them I guess.
> Why is this an interesting problem? What do we hope to learn from it?
Because it's a complicated puzzle, not necessarily because we hope to learn something from it. Which could happen, but it's definitely not the primary goal here.
> 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.
That's only true for sufficiently large N, large enough to encode the halting paradox. (How large is that N? It's larger than 5!) Smaller N can and do fall to systematic methods.
> (x) = (5x+18)/3 if x = 0 (mod 3),
The second = should be \equivalent. This is a rare case where that actually matters, because is being used in both non-modular integer operations (divide by 3) and modular operations (where division by 3 is not defined).
Can someone explain how there can a finite number of rules ?
Could the rule "If it's a 0, change it to 1 and move 3 squares to the left" produce a different result than when moving 4 squares, or is that not the case ?
(A TM rule has one sub-rule for each valid value / symbol)
Turing machines are characterised by the number of values (or symbols) and the number of rules (or states) (and technically the number of directions but TMs are generally one-dimensional). The Busy Beaver game fixes the number of symbols to 2, and only varies the number of states e.g. BB(3) is played on 3-states 2-symbols turing machines.
Thus the number of possible rules in BB(n) (n-states 2 symbols turing machine) is necessarily limited, to (4n + 4)^2n.
You can only ever move one step to the left or right. If you want to move multiple steps, you need multiple states to use as a counter, or set up the tape a specific way ahead of time so you know when to stop moving.
[+] [-] pvg|1 year ago|reply
And for leisure-class beavers, some big related threads from earlier this year:
https://news.ycombinator.com/item?id=40453221
https://news.ycombinator.com/item?id=38113792
https://news.ycombinator.com/item?id=37910297
[+] [-] inhumantsar|1 year ago|reply
I can't not find this phrase funny. out of context it reads like something out of Terry Pratchett or Douglas Adams.
[+] [-] unknown|1 year ago|reply
[deleted]
[+] [-] tromp|1 year ago|reply
One such variant 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), 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
[+] [-] anandijain|1 year ago|reply
I found this https://oeis.org/A141475, but it gives 27 trillion for 5.
[+] [-] passion__desire|1 year ago|reply
[+] [-] titanomachy|1 year ago|reply
[+] [-] jebarker|1 year ago|reply
[+] [-] danavar|1 year ago|reply
[+] [-] optimalsolver|1 year ago|reply
What's the payoff here?
I would rather someone of the intellectual calibre you describe work on problems more relevant to improving the world.
[+] [-] smokel|1 year ago|reply
For a modern version of the paper with some additional notes, see https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...
[+] [-] kryptiskt|1 year ago|reply
Note that there have been computer-assisted proofs before (four-color theorem, Kepler's conjecture), but those were not done in a formally verified setting until later.
[+] [-] nickdrozd|1 year ago|reply
By the way, there is an extremely stupid but disturbingly widespread idea that humans are able to just intuit solutions to the halting problem, using the mind's eye or quantum mechanics in the brain or whatever. Needless to say, this did not factor into the proof.
[+] [-] wodenokoto|1 year ago|reply
[+] [-] LegionMammal978|1 year ago|reply
> Prediction 5. It will never be proved that Σ(5) = 1,915 and S(5) = 2,358,064. (Or, if any larger lower bounds are ever found, the new values may be substituted into the prediction.)
> Reason: 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.
Luckily, this prediction did not come to pass, but only by a margin of one extra state.
[0] Allen Brady, "The Busy Beaver Game and the Meaning of Life", in Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey, Oxford University Press, 1988, pp. 259–277. This chapter can also be found in the 2nd ed., Springer, 1995, pp. 237–254.
[+] [-] Sniffnoy|1 year ago|reply
For the practical sense, other commenters have already replied.
For the mathematical sense, I would say it would be pretty surprising to me if BB(5) had been undecidable -- 5 states and 2 symbols is just so few with which to try to encode undecidable behavior.
However, it's worth noting that as a consequence of the incompleteness theorem, there must be some n such that standard mathematics cannot prove the value of BB(n). And in recent years various people have been working on finding such n and seeing how low they can get the number. The current record[0] is 745.
I expect that record can be probably be brought lower (more easily than the record for computing BB can be brought higher!), but even so, that's a lot of distance between 5 (the highest we know) and 745 (the lowest we know to be unknowable).
[0]This is the current record both for ZFC and for PA, in case you're wondering what I mean by "standard mathematics"... so it at least ought to be possible to bring it down further for PA! I think so far nobody's found a way to do better for PA than for ZFC, even though, like, that has to be possible, right?
[+] [-] tromp|1 year ago|reply
> But just four days ago, mxdys and another contributor known as Racheline discovered a barrier for BB(6) that seems insurmountable: a six-rule machine whose halting problem resembles a famously intractable math problem called the Collatz conjecture. Connections between Turing machines and the Collatz conjecture date back to a 1993 paper by the mathematician Pascal Michel, but the newly discovered machine, dubbed “Antihydra,” is the smallest one that appears unsolvable without a conceptual breakthrough in mathematics.
[+] [-] phaedrus|1 year ago|reply
I find it interesting that the description of Brady's program to optimize search for BB(4) by cutting out search subtrees whose differences don't matter is fairly close to a description of what I did to make my program fast.
[+] [-] ks2048|1 year ago|reply
Edit: number of TM for n states: (4n + 1)^(2n). Found this (for smaller n), which is the kind of analysis I was curious about: https://github.com/LukasKalbertodt/beaver
[+] [-] srcreigh|1 year ago|reply
[+] [-] openasocket|1 year ago|reply
When talking about the limits of human knowledge, I often think about the theorems that are provable, but so complex that no human being could understand them. Probably the most complex proof we have is the classification of finite simple groups, which is thousands upon thousands of pages, and there is probably very few or no people on Earth that fully understand all of it.
As the article suggests, BB(6) could be undecidable. But it could also have a proof millions of pages long, beyond the reach of humanity.
[+] [-] DowsingSpoon|1 year ago|reply
[+] [-] lkuty|1 year ago|reply
[+] [-] MrCheeze|1 year ago|reply
[+] [-] GTP|1 year ago|reply
Because it's a complicated puzzle, not necessarily because we hope to learn something from it. Which could happen, but it's definitely not the primary goal here.
[+] [-] lupire|1 year ago|reply
> 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.
That's only true for sufficiently large N, large enough to encode the halting paradox. (How large is that N? It's larger than 5!) Smaller N can and do fall to systematic methods.
> (x) = (5x+18)/3 if x = 0 (mod 3),
The second = should be \equivalent. This is a rare case where that actually matters, because is being used in both non-modular integer operations (divide by 3) and modular operations (where division by 3 is not defined).
[+] [-] Jean-Papoulos|1 year ago|reply
[+] [-] masklinn|1 year ago|reply
- set the current cell’s value
- move by one cell
- switch to the next rule (or halt)
(A TM rule has one sub-rule for each valid value / symbol)
Turing machines are characterised by the number of values (or symbols) and the number of rules (or states) (and technically the number of directions but TMs are generally one-dimensional). The Busy Beaver game fixes the number of symbols to 2, and only varies the number of states e.g. BB(3) is played on 3-states 2-symbols turing machines.
Thus the number of possible rules in BB(n) (n-states 2 symbols turing machine) is necessarily limited, to (4n + 4)^2n.
[+] [-] hmry|1 year ago|reply
[+] [-] seeknotfind|1 year ago|reply
[+] [-] jl6|1 year ago|reply
BB(1) = 1
BB(2) = 4
BB(3) = 6
BB(4) = 13
They just proved that BB(5) = 47,176,870.
It is known that BB(6) must be at least 10^10^...^10 (a tower of exponents fifteen levels high).
https://en.wikipedia.org/wiki/Busy_beaver#Known_values_for_%...
[+] [-] wayeq|1 year ago|reply
my team has also proved this via our production codebase
[+] [-] kaptainscarlet|1 year ago|reply
[+] [-] unknown|1 year ago|reply
[deleted]
[+] [-] bryan0|1 year ago|reply
[+] [-] unknown|1 year ago|reply
[deleted]
[+] [-] etx|1 year ago|reply
[deleted]
[+] [-] cmdrriker|1 year ago|reply
[deleted]
[+] [-] unknown|1 year ago|reply
[deleted]
[+] [-] unknown|1 year ago|reply
[deleted]