Determination of the fifth Busy Beaver value

Abstract

The Busy Beaver value $S(n)$ is the maximum number of steps that an $n$-state 2-symbol Turing machine can perform from the all-zero tape before halting. $S$ was historically introduced by Tibor Radó in 1962 as one of the simplest examples of an uncomputable function. We prove that $S(5) = 47,176,870$ using the Coq proof assistant. The proof enumerates $181,385,789$ Turing machines with 5 states and, for each machine, decides whether it halts or not. Our result marks the first determination of a new Busy Beaver value in over 40 years and the first Busy Beaver value ever to be formally verified, attesting to the effectiveness of massively collaborative online research (bbchallenge$.$org).

Figures (18)

• Figure 1: Transition table and space-time diagrams of the 5-state 2-symbol Busy Beaver winner, which halts after 47,176,870 steps. See https://bbchallenge.org/1RB1LC_1RC1RB_1RD0LE_1LA1LD_---0LA.
• Figure 2: Transition table and space-time diagrams of the 2-state 4-symbol Busy Beaver winner, which halts after $3{,}932{,}964$ steps. See https://bbchallenge.org/1RB2LA1RA1RA_1LB1LA3RB---.
• Figure 3: First-level children of the Tree Normal Form (TNF) enumeration of 5-state 2-symbol Turing machines: each node is a Turing machine, nonhalting machines are leaves of the tree. Internal nodes are halting machines, i.e. machines eventually reaching an undefined transition (highlighted in magenta), and their children correspond to all the ways to define this undefined transition. By symmetry, at the first level of the TNF tree, we can ignore machines taking a left move. The two halting machines at the first level of the tree each have 12 children, corresponding to all the choices in $\{\texttt{0}\xspace,\texttt{1}\xspace\}\times\{\text{R},\text{L}\}\times\{\text{{A}\xspace},\text{{B}\xspace},\text{{C}\xspace}\}$ for defining the magenta transition. Note that, in this case, the choice of states is reduced from $\{\text{{A}\xspace},\text{{B}\xspace},\text{{C}\xspace},\text{{D}\xspace},\text{{E}\xspace}\}$ to $\{\text{{A}\xspace},\text{{B}\xspace},\text{{C}\xspace}\}$ in order to prevent constructing machines that are only a permutation of one another.
• Figure 4: Space-time diagrams of the first 45 steps of a Cycler, https://bbchallenge.org/1RB---_0RC0LE_1LD0LA_1LB1RB_1LC1RC (left) and of the first 45 steps of a Translated Cycler, https://bbchallenge.org/1RB---_1LB1LC_0RD0RC_1LE1RE_1LA0LE (right). Cyclers are machines that eventually repeat the same configuration forever. Translated Cyclers are machines that eventually repeat the same configuration forever, but translated in space. We refer to these two types of machines as loops.
• Figure 5: Illustration of Lemma \ref{['lem:vector']}: head-only space-time diagram showing transcript repetition C1 A1 E0 D0C1 A1 E0 D0. Coordinates $p_0 = (t_0,g(t_0))$ correspond to the beginning of the first repetition, and $p'_0 = (t_0',g(t_0'))$ of the second. We can easily show that the machine state is the same state, C, at position $p^*$ and as at position $p_0'$, Lemma \ref{['lem:vector']} Point \ref{['lem:vector:pt2']}. Less immediate, in this case, using $p_k$ and $p'_k$, we can show that positions $p^*$ and $p_0'$ also share same read-symbol (depicted as ? to signify that it is less immediate to show), which is the symbol outputted after $p_k$ and $p_k'$, Lemma \ref{['lem:vector']} Point \ref{['lem:vector:pt4']}.

Theorems & Definitions (31)

• Theorem 1.1: : Lemma BB5_value
• Theorem 1.2: : Lemma BB2x4_value
• Conjecture 1.1: Antihydra does not halt
• Lemma 4.1
• proof
• Definition 4.1: Loops
• Lemma 4.2
• proof
• Theorem 4.1: Loops
• proof