I know that the halting problem is undecidable in general but there are some Turing machines that obviously halt and some that obviously don't. Out of all possible turing machines what is the smallest one where nobody has a proof whether it halts or not?
The largest Turing machines for which the halting problem is decidable are:
$TM(2,3), TM(2,2), TM(3,2)$ (where $TM(k,l)$ is the set of Turing machines with $k$ states and $l$ symbols).
The decidability of $TM(2,4)$ and $TM(3,3)$ is on the boundary and it is difficult to settle because it depends on the Collatz conjecture which is an open problem.
See also my answer on cstheory about Collatz-like Turing machines and "Small Turing machines and generalized busy beaver competition" by P. Michel (2004) (in which it is conjectured that $TM(4,2)$ is also decidable).
Kaveh's comment and Mohammad's answer are correct, so for a formal definition of the standard/non-standard Turing machines used in this kind of results see Turlough Neary and Damien Woods works on small universal Turing machines, e.g. The complexity of small universal Turing machines: a survey (Rule 110 TMs are weakly universal).
I would like to add that there are some Turing Machines for which the Halting problem is independent of ZFC.
For instance take a Turing machine which looks for a proof of contradiction in ZFC. Then if ZFC is consistent, it won't halt, but you cannot prove it in ZFC (because of Gödel's second incompleteness theorem).
So it is not only a matter of not having found a proof yet, sometimes proofs don't even exist.
Overview of Turing Machine decidability starting on the a blank tape (Busy Beaver style)
For the blank tape input only:
- 4-state machines: all decided in 1983
- 5-state machines: as of 2023 it is generally believed that all 5-state machines have been decided pending only better verification and perhaps boring proofs analogous to other existing proofs
- 6-state machines: might quite possibly remain forever open however, see the BB(6) section below
The best overview of "lists of unproven machines" by various sources currently is this page from the "The Busy Beaver Challenge" (bbchallenge): https://bbchallenge.org/story#skelets-43-undecided-machines As of 2023 The bbchallenge is the most visible ongoing project to calculate BB(5), the Busy Beaver "shift" function of 5 AKA
s(5) in some older literature, which counts how many steps a Turing machine runs for on a tape full of 0's before halting. Non-halting ones are excluded. So calculating BB(5) implies solving the halting problem for every single Turing machine with 5 states.
As highlighted by the bbchallenge, it also depends a lot on what you consider "verified", ranging from manual proof, to unverified programmatic checks, to formal proofs.
One of the major features of the bbchallenge are deciders. Deciders are programs that attempt to decide if a large number of Turing machines halt or not. But note that all deciders seem to be parameterized with "search depth like parameters", so it is not easy to be sure if more would be solved with larger parameters and more computational time. And in is a notable example of that some rare cases, time can get ridiculously large, requiring more advanced/specialized techniques in practice for proving specific machines, Skelet #1 below.
Back in 2003, Skelet produced a list of only 43 machines that he was not able to decide with a large formally unverified Pascal decider program, plus a few manual proofs. That list has generally considered to contain some of the "most likely unproven/hardest to prove ones".
Then more recently and independently, bbproject contributors also managed to decide all machines except 34 with deciders, but with much better review/verification procedures: https://discuss.bbchallenge.org/t/the-30-to-34-ctl-holdouts-from-bb-5/141/3
So it is interesting to see that both approaches found about ~30-40 machines that were not "easily" automatically provable and required manual proofs. This is of course where the gold lies, as these non-automatable machines are the ones most likely to represent "complex theorems worthy of mathematician's brain time", see also: ""Real" open conjectures reduced to Turing Machines below."
If these are worth a mathematician's brain time or not, is another story. Some of the machines appear to require computational + brain approaches, e.g. Skelet #1, which while epic, might not hold that much insight into Life, the Universe and Everything. Some however will hold deeper meaning of course.
Skelet's 43 holdouts
Skelet's holdouts were initially published at: https://skelet.ludost.net/bb/nreg.html
Dan Briggs manage to prove some of Skelet's 43 never halt circa 2021: https://github.com/danbriggs/Turing/blob/master/paper/HNRs.pdf
The BB challenge also solved some with their own deciders: https://bbchallenge.org/skelet
The "individual machines" section of the bbchalenge Discuss is likely best way to find an publish state of the art, it is basically the "Journal of BB(5) Research" if you will! https://discuss.bbchallenge.org/c/individual-machines/7 Some early movements occasionally also happen on Discord, go figure: https://discord.com/channels/960643023006490684/1026577255754903572 Notably, #1 and #34 also fell:
- #1 https://www.sligocki.com/2023/03/13/skelet-1-infinite.html | https://discuss.bbchallenge.org/t/skelet-1-is-a-translated-cycler-coq-agrees/166
#1 was particularly epic, a shifted cycle with cycle of about ~8 billion steps.
It seems likely that the bbproject managed to resolve all of the holdouts as mentioned at: http://discuss.bbchallenge.org/t/the-30-to-34-ctl-holdouts-from-bb-5/141/4?u=cirosantilli and surrounding posts.
It currently looks like will likely never know BB(6). Or it would require a CERN-like mega-project, or AGI. Therefore if you are looking for some small Turing machines to prove, going through BB(6) one a time, trying every known decider on it, and failing that going for manual proof seems like a good approach!
A good argument we think BB(6) might never be known is that $BB(6) \ge 10 \uparrow \uparrow 15$, overview: https://www.sligocki.com/2022/06/21/bb-6-2-t15.html (Pavel Kropitz, 2022) i.e. Pavel came up with a machine he managed to prove halts after that time/many 1's written.
Therefore, if there are any BB(6) holdouts that take nearly as much computation time to decide, we might really never solve them. Compare that e.g. to BB(5), where the current champion halts after ~47 million steps, but where Skelet #1 has a cycle of the order of billions.
"Real" open conjectures reduced to Turing Machines
Some mathematical problems can be reduced to deciding the halting problem of a specific Turing machine. The best example of this is perhaps Goldbach conjecture, where it is obvious how you can make a Turing machine that just walks every positive number one by one, tries every possible pair of smaller numbers that sum up to it, and checks if they are prime. Then it halts if no valid pair is found for a number, or continues to infinity otherwise.
Such Turing machines serve therefore as examples of "known hard to prove problems". Going down that route also allows to show that certain Turing machines are undecidable in a certain proof system, e.g. ZF. This is done by modelling the logic system itself with a Turing machine.
https://bbchallenge.org/story#what-is-known-about-bb is the best list available as of 2023:
- BB(15) is at least as hard as Erdős' conjecture on powers of 2: "for n > 8, there is at least one digit 2 in the base-3 representation of 2n". [Stérin and Woods, 2021]
- BB(27) is at least as hard as Goldbach conjecture: “for n > 2, every even integer is the sum of two primes” unverified construction [Aaronson, 2020]
- BB(744) is at least as hard as Riemann Hypothesis [Matiyasevich and O’Rear and Aaronson, unpublished]
- BB(748) is independent of ZF [O’Rear, unpublished]
- BB(5,372) is at least as hard as Riemann Hypothesis [Yedidia and Aaronson, 2016]
- BB(7, 910) is independent of ZFC [Yedidia and Aaronson, 2016]
Most/all of these proofs involved compiling down simple programming languages to Turing machines programmatically, see also: https://cs.stackexchange.com/questions/50815/compiler-that-compiles-to-a-turing-machine
It is worth noting however that not all mathematical problems can be directly reduced to a "simpler halting problem" (that does not directly involve proving another Halting problem). E.g. this is not the case for Collatz conjecture, as a counterexample would go off to infinity and you wouldn't be able to tell: https://mathoverflow.net/questions/309044/is-there-a-known-turing-machine-which-halts-if-and-only-if-the-collatz-conjectur Goldbach is fundamentally different from Collatz in that you can just try every smaller number and be done for each integer.
Some real cool but mostly philosophical aspects of such reductions are:
- they allow us to estimate how hard a conjecture might be to prove: the more states in the Turing machine the harder
- they might allow for automated proofs to be carried out via deciders. In this way, they can be seen as a sort of "normal form" for large chunks of mathematics, much like 3SAT is a kind of normal form for NP.
Blank tapes vs arbitrary tapes
As highlighted by Marzio, the question of "decide every N-state Turing machine for every possible input" has already reached the wall basically:
- 3 states: decidable
- 4 states: unknown believed to be decidable
- 5 states: a Collatz-like problem
- 10 states: Collatz itself
- 15 states: Turing machine simulation (Universal Turing machine)
These numbers were extracted from the following answers which give their references:
- What's the simplest noncontroversial 2-state universal Turing machine?
- What is the "nearest" problem to the Collatz conjecture that has been successfully resolved?
Also note that the second image is already outdated as we have a 15-state universal machine as per first image, just it simulates slower than the previously known 19-state one.
While those could potentially be reduced slightly if an even smaller machine is found, we are already basically bricked at 5 states in terms of what we can prove.
This is what makes the blank-tape only problem more compelling to me. It is fundamentally simpler, as we don't have to consider infinitely many inputs for each machine: one machine, one input, can I decide it.
As a result, we get to zoom in much more, and the boundary between decidable, hard maths problem and undecidable has humongous gaps that beg to be improved. Notably, given that we got away with only 30-40 manual proofs for BB(5), it is not clear if BB(6) will present fundamentally hard maths problems or not. What about BB(7)? And so on. Because now we are at BB(15), which is a monumental gap away from BB(5).
No one has a proof whether Universal Turing machine halts or not. In fact, such proof is impossible as a result of the undecidability of the the Halting problem . The smallest is a 2-state 3-symbol universal Turing machine which was found by Alex Smith for which he won a prize of $25,000.
an inexactly phrased but reasonable general question that can be studied in several particular technical ways. there are many "small" machines measured by states/symbols where halting is unknown but no "smallest" machine is possible unless one comes up with some justifiable/quantifiable metric of the complexity of a TM that takes into account both states and symbols (apparently nobody has proposed one so far).
actually research into this problem related to Busy Beavers suggests that there are are many such "small" machines lying on a hyperbolic curve where $x \times y$, $x$ states and $y$ symbols, is small. in fact it appears to be a general phase transition/boundary between decidable and undecidable problems.
this new paper Problems in number theory from busy beaver competition 2013 by Michel a leading authority exhibits many such cases for low $x,y$ and shows the connection to general number theoretic sequences similar to the Collatz conjecture.