Determination of the fifth Busy Beaver value
This solves a long-standing open problem in theoretical computer science, providing a concrete result in computability theory.
The authors determined the fifth Busy Beaver value, S(5) = 47,176,870, by enumerating and analyzing 181,385,789 Turing machines using the Coq proof assistant, marking the first new value in over 40 years and the first formally verified one.
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).