The fifth busy beaver value
Among all Turing machines with 5 states and 2 symbols that halt when started on a blank tape, what is the largest number of steps taken before halting? Determine and prove that every 5-state machine that runs longer never halts.
History and references
Solved in 2024 by The bbchallenge collaboration.
Tibor Radó defined the busy beaver functions in 1962 as simple examples of uncomputable functions, since they grow faster than any computable function. Around 1990 Heiner Marxen and Jürgen Buntrock found a 5-state machine that halts after 47,176,870 steps, and it became the conjectured champion. Proving it optimal meant deciding, for each of about 181 million 5-state machines, whether it halts. The online bbchallenge collaboration completed this in July 2024 with a proof formalized in the Coq (now Rocq) proof assistant, establishing , and posted a paper describing the proof in 2025. It was the first new busy beaver value in over 40 years and the first ever to be formally verified, and the 6-state value is unknown and known to be astronomically large.
References
Solutions 0
Sign in or create an account to publish a solution