So we were just lucky that all non-halting programs of length 5 just happened to be provably non-halting?
> 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.
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?
If you can encode a problem in n states, and you know BB(n), then, as you say, you could use that to solve the problem. Trouble is, how do you know BB(n)? In reality, the only way to determine BB(n) is to go and solve all such problems; there isn't any other easier method that you can apply that would then let you get answers for these problems as a consequence.
So, the value of BB(n) will always be a summation of "we did all the hard work of solving all the n-state problems", not something you do separately to get those answers out.
Actually, just as you can do bijective base-b [0], you can also do bijective Zeckendorf (using 1 and 2 with no two consecutive 1s). Although, as happens with bijective binary, bijective Zeckendorf is closely tied to ordinary Zeckendorf, so it doesn't offer much new. But bijective dual Zeckendorf doesn't work -- lots of numbers can't be represented!
One more fun fact about Zeckendorf and dual Zeckendorf: Write n>0 in Zeckendorf, and count how many zeroes it ends in. This will be even if the dual Zeckendorf representation of n ends in a 1, and odd if it ends in a 0. Similarly, if you write n in dual Zeckendorf and count how many 1s it ends in, this will be even if the (ordinary) Zeckendorf representation ends in a 0 and odd if it ends in a 1.
This isn't disagreeing with what I was saying, though; I said incompleteness requires there is some such n, and then also said what we know about the record, I didn't say the record comes from a Gödel sentence.
Hope my comment addresses a common confusion despite its unnecessarily corrective tone.
But for any given TM, can we decide whether it is provable or not? Or will we meet some that we will never know if we can solve or not?
Insofar as we are given provability, we can solve halting.
Would you be brave enough to say the same thing about BB(6) or BB(7)?
Because that one needs to be solved for BB(6) already: https://wiki.bbchallenge.org/wiki/Antihydra
Considering how we made basically no real progress on it mathematically in a whole generation, solving BB(6) within the next decades would be a miracle, and I would bet a lot against it.
I can't see us EVER getting to BB(10), no matter how advanced humanity grows (and it would be meaninglessly large anyway).
I think 765 is just a huge overestimation based on the fact that it is somewhat straightforward to construct.
But yes, I'd be very surprised if Collatz were actually undecideable, even if it's well beyond the reach of current mathematics.
I agree with your statements about BB(10) and BB(6), but they just aren't very relevant. I agree those involve extremely difficult problems likely well beyond the reach of current mathematics, but I'd still be very surprised to find anything undecideable in there. There's a big difference between being truly undecideable and merely well beyond the reach of current mathematics!
(Also, the current record for undecideability is 745, or 765.)
> 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.
Does this mean a BB(6) machine which resembles Collatz is testing all possible values as part of it program and not part of anything on the tape (since the tape start out empty)?
For collatz, the empty input machine loops over all natural numbers and halts if it finds one which doesn’t eventually reach 1.
To prove that it never halts, you’d have to prove the collatz conjecture. Otherwise you’d have to find the smallest counter example of the collatz conjecture.
Collatz-TM connections have been investigated much earlier.
My fav is John Conway in 1972, who showed that the generalized Collatz problem is undecidable.[1]
[1]: https://en.wikipedia.org/wiki/Collatz_conjecture#Undecidable...