The Busy Beaver Problem
Abstract
Alan Turing proved in 1936 that no program can decide, in general, whether an arbitrary program will halt. That result is abstract; the busy beaver problem makes it concrete and even competitive. Take the simplest possible computers, Turing machines with just a handful of states, and ask which one runs the longest before stopping. The answer is a specific finite number for each size, and yet the sequence of those numbers grows faster than any computable function and eventually becomes provably impossible to determine. In July 2024 an online collaboration of amateurs settled the five-state case, a value that had resisted proof for over forty years, and the six-state case is now entangled with open problems in number theory.
Radó’s Game
In 1962 the Hungarian mathematician Tibor Radó, at Ohio State, proposed a game in a paper titled “On Non-Computable Functions”. Consider Turing machines with n states, working on an initially blank tape of 0s, each machine allowed to write 0s and 1s and move left or right. Some of these machines run forever; ignore those. Among the ones that eventually halt, which writes the most 1s, and which runs for the most steps before stopping? Radó named the answers Σ(n), the busy beaver function (most 1s), and S(n) (most steps). The “busy beaver” for size n is the hardest-working machine that still manages to stop.
The definitions look innocent, and for tiny n they are. But Radó proved that Σ(n) grows faster than any computable function. No formula, no algorithm, nothing that a computer could ever run will keep pace with the busy beaver numbers as n increases. This is the halting problem wearing a number’s clothes: if you could compute S(n), you could decide whether any small machine halts (run it for S(n) steps; if it has not stopped, it never will), and Turing proved you cannot. Uncomputability, usually stated as an abstract impossibility, here becomes a specific sequence of integers that no method can generate.
The Numbers That Can Be Known
For small machines the beavers can be hunted by hand and by computer search:
- BB(1) = 1 (one 1, halting in 1 step)
- BB(2) = 4 ones, 6 steps
- BB(3) = 6 ones, 21 steps
- BB(4) = 13 ones, 107 steps
Then a cliff. The five-state case exploded. The best known five-state machine writes 4,098 ones and runs for 47,176,870 steps, a value conjectured for decades. The difficulty is not finding candidate machines but proving that none of the millions of five-state machines runs even longer. Most halt quickly or obviously loop, but a stubborn residue of machines have to be individually proven non-halting, and some of them encode behavior resembling open mathematical conjectures. Proving BB(5) meant proving that every one of those holdouts never stops.
An Internet of Amateurs Closes the Case
The five-state proof was completed in July 2024, not by a university team but by bbchallenge, an online collaboration of amateur mathematicians and programmers who had organized around the problem, and the argument was verified in the Coq proof assistant so that the conclusion did not rest on trusting anyone’s code. BB(5) = 47,176,870 became a theorem. It is a modern echo of an old pattern in this field: a distributed group of enthusiasts, coordinating over the internet and leaning on a machine-checked proof, closing a question that had sat open since the 1980s.
Six states is another world entirely. The best known lower bound for BB(6) is not a number anyone can write out; it exceeds 2↑↑↑5, a tower of exponentials in Knuth’s up-arrow notation, a magnitude with no physical meaning. Worse, some six-state machines have been shown to halt if and only if certain unsolved conjectures in number theory are true, which means that pinning down BB(6) may require resolving those conjectures first. The busy beaver has walked from a recreational puzzle into the position of a yardstick for the limits of provability: there exists some n, not enormous, beyond which the value of BB(n) is independent of the standard axioms of mathematics and can never be proven at all. Radó’s game turned Gödel’s incompleteness into a horizon you can count toward.