Contents
Last update: October 2021

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:

1. To enumerate Turing machines without repetition.
2. To simulate Turing machines efficiently.
3. To recognize non-halting Turing machines.
Note that these procedures are often mixed together in real programs, as follows: A tree of transition tables is generated, and, as soon as some transitions are defined, the corresponding Turing machine is simulated. If the definition of a new transition is necessary, the tree is extended. If the computation seems to loop, a proof of this fact is provided.

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.

• For (4,2)-TM:
The determination of the value of Rado's noncomputable function Sigma(k) for four-state Turing machines
Mathematics of Computation 40 (162), April 1983, 647-665.

• Machlin R. and Stout Q.F. (1990)
The complex behavior of simple machines
Physica D 42, June 1990, 85-98.

• For (5,2)-TM:
• Marxen H. and Buntrock J. (1990)
Attacking the Busy Beaver 5
Bulletin of the EATCS No 40, February 1990, 247-251.

• Hertel J. (2009)
Computing the uncomputable Rado sigma function
The Mathematica Journal 11 (2), 2009, 270-283.

• For (2,3)-TM:
• Lafitte G. and Papazian C. (2007)
The fabric of small Turing machines
in: Computation and Logic in the Real World, Proceedings of the Third Conference on Computability in Europe, June 2007, 219-227.

• Page about Macro Machines on Marxen's website.

• Articles by James Harland:
• Harland J. (2016)
Busy beaver machines and the observant otter heuristic (or how to tame dreadful dragons)
Theoretical Computer Science 646, 2016, 61-85.
Preprint available at arXiv:1602.03228.

• Harland J. (2016)
Generating candidate busy beaver machines (or how to build the zany zoo)
Available at arXiv:1610.03184.

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:
• 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,
• . . .
When a machine Mi stops, we add it to a list of machines that stop when they are launched on a blank tape.

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 A gives us a computably enumerable list of the Turing machines that stop when they are launched on a blank tape.

• Algorithm B gives us a computably enumerable list of the Turing machines that provably do not stop on a blank tape.

We mix together these two algorithms, by a procedure called dovetailing, to get Algorithm C, as follows.
Algorithm C.
• 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,
• . . .
Algorithm C gives us simultaneously both the computably enumerable lists provided by Algorithm A and 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:

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 states to 1919, in September 2016.
He improved later the number of states to 748.
His machines enumerate 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.

• There is another proof of unprovability, based on Kolmogorov complexity.

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:

• Chaitin G. (1987)
Computing the busy beaver function
Open Problems in Communication and Computation, Springer, 1987, 108-112.
Reprinted in: Information, Randomness and Incompleteness, World Scientifics, 2nd Ed., 1990.

• Boolos G.S., Burgess J.P. and Jeffrey R.C. (2002)
Computability and Logic, 4th Ed., Cambridge, 2002, pp. 40-44 and 227-230 (They note that n(T) < 10^10^10^10^10^10^10^10^10^10).

• Lafitte G. (2009)
Busy beavers gone wild
in: The Complexity of Simple Programs 2008, EPTCS 1, 2009, 123-129.

Tables normalization

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:
• it enters states in the following order: A, B, C, ...

• it writes symbols in the following order: 0, 1, 2, ...
So, normally, the first transition is A0 --> 1RB or A0 --> 0RB.

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

 A0 A1 A2 A3 B0 B1 B2 B3 sigma(M) s(M) 3RB 3RA 3RA 1LA 3LB 2RB 2LH 3LA 2,050 3,932,964 TNF: 1RB 2LA 1RA 1RA 1LB 1LA 3RB 1RH 2,050 3,932,964

Turing machines with 2 states and 5 symbols

 A0 A1 A2 A3 A4 B0 B1 B2 B3 B4 sigma(M) s(M) 1RB 4LA 1LA 2LA 1RA 3LA 1RH 1RA 2RA 4RB 11,120 148,304,214 TNF: 1RB 3LA 4LA 1RA 1LA 2LA 1RH 4RA 3RB 1RA 11,120 148,304,214 4RB 2LA 4LA 4RA 3LA 1LA 4LA 4RA 3RB 3LH 3,685 16,268,767 TNF: 1RB 3LA 4LA 1RA 1LA 2LA 1RH 1LA 3RB 1RA 3,685 16,268,767 4LB 1RH 2RA 0LB 3LB 2RA 3LB 3RB 2LB 1LB 4,099 15,754,273 TNF: 1RB 3RB 2LA 0RB 1RH 2LA 4RB 3LB 2RB 3RB 4,099 15,754,273

Turing machines with 2 states and 6 symbols

 A0 A1 A2 A3 A4 A5 B0 B1 B2 B3 B4 B5 sigma(M) s(M) 1RB 4LA 1RA 5LB 1RA 3LB 1LB 1LA 5LA 2LA 2RB 1RH 15,828 493,600,387 TNF: 1RB 2LA 1RA 1RA 5LB 4LB 1LB 1LA 3RB 4LA 1RH 3LA 15,828 493,600,387 4RB 4RA 4RA 1LA 1LA 1LB 4LB 2RB 5LB 3RA 3LA 1RH 10,249 98,364,599 TNF: 1RB 3LA 3LA 1RA 1RA 3LB 1LB 2LA 2RA 4RB 5LB 1RH 10,249 98,364,599 5RB 5RA 3RH 1RB 3LA 1LA 4LB 1RB 4LH 2RA 5LB 5LA 10,574 94,842,383 TNF: 1RB 3LA 4LA 1RA 3RB 1RH 2LB 1LA 1LB 3RB 5RA 1RH 10,574 94,842,383

Turing machines with 3 states and 4 symbols

 A0 A1 A2 A3 B0 B1 B2 B3 C0 C1 C2 C3 sigma(M) s(M) 1RB 2LC 0LC 0RA 3LC 2RC 1LB 0RC 1RA 0LB 1RH 0RB 17,323 262,759,288 TNF: 1RB 3LC 0RA 0LC 2LC 3RC 0RC 1LB 1RA 0LB 0RB 1RH 17,323 262,759,288

Turing machines with 4 states and 3 symbols

 A0 A1 A2 B0 B1 B2 C0 C1 C2 D0 D1 D2 sigma(M) s(M) 0RB 1RH 2LD 2LA 2RD 2RC 2RB 2RC 1LC 2LA 1RB 2LC 15,008 250,096,776 TNF: 0RB 1LD 1RH 1LA 1RC 1RD 1RB 2LC 1RC 1LA 1LC 2RB 15,008 250,096,776