We prove that S(5) = 47,176,870. The Busy Beaver value S(n) gives the maximum number of steps a halting n-state 2-symbol Turing machine can perform from the all-0 tape before halting and S was historically introduced as one of the simplest examples of a noncomputable function.
Using the Coq proof assistant, we enumerate 181,385,789 5-state Turing machines, and for each, decide whether it halts or not. Most of these machines are decided using new algorithms that simplify the halting problem by building Finite State Automata to approximate the machine's set of reachable configurations. For 13 challenging Sporadic Machines, we provide individual Coq proofs of nonhalting.
Our result marks the first determination of a new Busy Beaver value in over 40 years, leveraging Coq's computing capabilities and demonstrating the effectiveness of collaborative online research.
=== Hybrid talk ===
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Meeting ID: 871 4336 5195
Passcode: 541180
