Kavli Affiliate: Chris Xu
| First 5 Authors: The bbchallenge Collaboration, The bbchallenge Collaboration, , ,
| Summary:
We prove that $S(5) = 47,176,870$ using the Coq proof assistant. 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, and $S$ was
historically introduced by Tibor Rad’o in 1962 as one of the simplest examples
of an uncomputable function. 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).
| Search Query: ArXiv Query: search_query=au:”Chris Xu”&id_list=&start=0&max_results=3