Advanced topics on Busy Beavers
The methods used to find busy beavers
Busy beavers and unprovability
Last update: August 2017
The methods used to find busy beavers
The machines presented in these pages were discovered by means of computer programs. These programs contain procedures that achieve the following tasks:
If the purpose is to prove a value for the busy beaver functions, then all Turing machines in a class have to be studied. The machines that pass through the three procedures above are either halting machines, from which the better one is selected, or holdouts waiting for better programs or for hand analyses.
If the purpose is to find lower bounds, a systematic enumeration of machines is not necessary. Terry and Shawn Ligocki said they used simulated annealing to find some of their machines.
The following references can be consulted for more information.
Busy beavers and unprovability
Let S(n) = S(n,2) be Rado's busy beaver function. We know that S(2) = 6, S(3) = 21, S(4) = 107, and we can hope to prove that S(5) = 47,176,870. As we will see below, the fact that the busy beaver function S is not computable implies that it is not possible to prove that, for any natural number n, S(n) has its true value.
Formally, we have the following theorem.
Theorem. Let T be a well-known mathematical theory such as Peano arithmetic (PA) or Zermelo-Fraenkel set theory with axiom of choice (ZFC). Then there exist numbers N and L such that S(N) = L, but the sentence "S(N) = L" is not provable in T.This theorem is an easy consequence of the following proposition.
Proposition. Let T be a well-known mathematical theory such as PA or ZFC. Then there exists a Turing machine with two symbols M that does not stop when it is launched on a blank tape, but the fact that it does not stop is not provable in T.
Proof of the theorem from the proposition. Let M be the Turing machine given by the proposition, let N be the number of states of M, and let L = S(N). Then, to prove that "S(N) = L", we have to prove that M does not stop. But, by the proposition, such a proof does not exist.
Proof of the proposition. This proposition is well-known and a one line proof can be given, as follows.
If all non-halting machines were provably non-halting, then an algorithm that gives simultaneously the computable enumeration of the halting machines and the computable enumeration of the provably non-halting machines would solve the halting problem on a blank tape.We give a detailed proof for nonspecialist readers.
Let M1, M2, . . . be a computably enumerable sequence of
all Turing machines with two symbols.
Such a sequence can be obtained as follows: we list machines according to their number of states, and, inside the set of machines with n states, we list the machines according to the alphabetical order of their transition tables.
Let T1, T2, . . . be a computably enumerable sequence of the
theorems of the theory T.
The existence of such a sequence is the main requirement that theory T has to satisfy in order that the proposition holds, and of course such a sequence exists for well-known mathematical theories such as PA or ZFC.
Now consider the following algorithms A and B.
Algorithm A. We launch the machines Mi on the blank tape as follows:
When a machine Mi stops, we add it to a list of machines that stop when they are launched on a blank tape.
- one step of computation of M1,
- 2 steps of computation of M1, 2 steps of computation of M2,
- 3 steps of computation of M1, 3 steps of computation of M2, 3 steps of computation of M3,
- . . .
Note that, given a machine M, by running Algorithm A we will know that M stops if M stops, but we will never know that M doesn't stop if M doesn't stop.
Algorithm B. We launch the algorithm that provides the computably enumerable sequence of theorems of theory T, and each time we get a theorem Ti, we look and see if this is a theorem of the form "The Turing machine M does not stop when it is launched on a blank tape". If that is the case, we add M to a list of Turing machines that provably do not stop on a blank tape.
Note that, given a machine M, by running Algorithm B we will know that M is provably non-halting if M is provably non-halting, but we will never know that M is not provably non-halting if M is not provably non-halting.
Now we have two algorithms, A and B, and
Algorithm C.Algorithm C gives us simultaneously both the computably enumerable lists provided by Algorithm A and Algorithm B.
- one step of Algorithm A, one step of Algorithm B,
- 2 steps of Algorithm A, 2 steps of Algorithm B,
- 3 steps of Algorithm A, 3 steps of Algorithm B,
- . . .
So Algorithm C gives us both the list of halting Turing machines and the list of provably non-halting Turing machines (on a blank tape).
Now we are ready to prove the proposition.
If all non-halting Turing machines were provably non-halting, then Algorithm C would give us the list of halting Turing machines and the list of non-halting Turing machines (on a blank tape). So, given a Turing machine M, by running Algorithm C, we would see M appearing in one of the lists, and we could settle the halting problem for machine M on a blank tape. So Algorithm C would give us a computable procedure to settle the halting problem on a blank tape. But it is known that such a computable procedure does not exist. Thus, there exists a non-halting Turing machine that is not provably non-halting on a blank tape.
Consider the Turing machine M given by the proposition: M does not stop when it is launched on a blank tape, but this fact is not provable in theory T. We can get an idea of what such a machine M looks like, as follows.
For example, M can be a machine that enumerates the theorems of theory T, and stops when it finds a contradiction (such that 0 = 1 if T is Peano arithmetic).
Then a proof within theory T that M does not stop would be a proof within theory T of the consistency of T, which is impossible by Gödel's Second Incompleteness Theorem (if theory T is consistent).
This gives another proof of the proposition, a shorter one, but resting on a big theorem.
Another example can be given using Gödel's First Incompleteness Theorem. If T is PA or ZFC, supposed to be consistent, the proof of this theorem provides a formula F that asserts its own unprovability. Thus F is true, but unprovable within theory T.
Consider the machine M that enumerates the theorems of theory T, and stops when it finds formula F.
Machine M does not stop, since F is unprovable, but a proof that it does not stop would be a proof that F is unprovable, so, since F is "F is unprovable", a proof of F, which is impossible, since F is unprovable.
As a third example, consider the machine M that enumerates the theorems of theory T (PA or ZFC, supposed to be consistent), and stops when it finds a formula F that says that M itself does not stop. Such a machine can be proved to exist by applying the Recursion Theorem to the function f such that machine Mf(x) stops if it finds a proof that machine Mx does not stop.
Then F is true, because, if F were false, then M would stop, so F would be a theorem of T, so F would be true. But F is unprovable, because since F is true, M does not stop, so F is not a theorem of theory T. So the fact that M does not stop is true and unprovable.
Note that, in these three examples of Turing machines M, the watched formulas are more and more complicated, and the theorems used to prove that M suits are more and more elementary.
Since May 2016, there are explicit constructions of Turing machines whose behaviors are independent of ZFC.
Adam Yedidia and Scott Aaronson gave, in May 2016, a Turing machine with 7910 states and two symbols such that it cannot be proved in ZFC that it never halts. They note that enumerating the theorems of ZFC would need a big number of states. They use a graph theoretic statement that Harvey Friedman proved to be equivalent to the consistency of a theory that implies the consistency of ZFC. By using a new high-level language that is easily compiled down to Turing machine description, they build a machine that would halt if it finds a counterexample to Friedman's statement.This is published in:
Adam Yedidia, Scott Aaronson,
A relatively small Turing machine whose behavior is independent of set theory,
Complex Systems 25 (4), 2016, 297-327.
Available on the Web.
S. O'Rear improved the number of state to 1919, in September 2016. His machine enumerates the theorems of a formal system which has the same power as ZFC.
See Scott Aaronson's blog for a general presentation.
Note that, if "S(N) = L" is a true sentence unprovable in theory T, then, for all m > L, "S(N) < m" is also a true sentence unprovable in theory T.
Note that the proposition is a special case of the following more general theorem.
Theorem. Let A be a set of natural numbers that is computably enumerable but not computable, and let T be a well-known mathematical theory such as PA or ZFC. Then there exists a natural number n such that the sentence "n is not a member of A" is true but not provable in theory T.The proof of this theorem is the same as above: if all natural numbers not in A were provably not in A, then the simultaneous enumerations of A and of natural numbers provably not in A would give a procedure that decides membership in A, contradicting the fact that A is not computable.
The proposition is gotten from this theorem by numbering the list of Turing machines, and by defining A as the set of numbers of Turing machines that stop on a blank tape.
The Kolmogorov complexity of a number is the length of the shortest program from which a universal Turing machine can output this number.
By Chaitin's Incompleteness Theorem, for any well-known mathematical theory T, there exists a number n(T) such that, for all numbers of complexity greater than n(T), the fact that they have complexity greater than n(T) is true but unprovable within theory T.
Chaitin's theorem also applies to the complexity defined as follows: The complexity of a number k is the smallest number n of states of a Turing machine with n states and two symbols that outputs this number k, written as a string of k symbols 1, when the machine is launched on a blank tape.
So there exists a number n(T) such that, for any number k of complexity greater than n(T), the sentence "the complexity of k is greater than n(T)" is true but unprovable within theory T. But "k > Sigma(n(T))" implies "the complexity of k is greater than n(T)", so, for any number k > Sigma(n(T)), "k > Sigma(n(T))" is true but unprovable within theory T.
For more details, see the following papers and books:
A permutation of states, or a permutation of symbols,
does not change the behavior of a Turing machine.
Suppose you get two Turing machines, taking the same time to stop on an initially blank tape. How to know whether these machines are essentially different, or they are just the same machine up to a permutation of states or symbols?
To settle this problem, you can normalize the table, putting it in tree normal form (TNF).
Since we are interested by the behaviors of Turing machines on an initially blank tape, the simplest rule is the following one:
When the Turing machine is launched on a blank tape:So, normally, the first transition is A0 --> 1RB or A0 --> 0RB.
- it enters states in the following order: A, B, C, ...
- it writes symbols in the following order: 0, 1, 2, ...
As an example, we give below the tables of the Turing machines as found by Terry and Shawn Ligocki, and their normalized versions as given in the present web pages.
Turing machines with 2 states and 4 symbols
Turing machines with 2 states and 5 symbols
Turing machines with 2 states and 6 symbols
Turing machines with 3 states and 4 symbols
Turing machines with 4 states and 3 symbols
Link to the home page of Pascal Michel