🦫 Determination of the fifth Busy Beaver value

The bbchallenge Collaboration, Justin Blanchard, Dan Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev (Skelet), Matthew L. House, Rachel Hunter, Iijil, Maja Kądziołka, Pavel Kropitz, Shawn Ligocki, mxdys, Mateusz Naściszewski, savask, Tristan Stérin, Chris Xu, Jason Yuen, Théo Zimmermann

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-0 tape before halting and $S$ was historically introduced by Tibor Radó 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 to ever be formally verified, attesting to the effectiveness of massively collaborative online research (bbchallenge.org).

Pre-Preprint (v0.99)

• August 12, 2025: version 0.99 of the preprint released (integrating feedback received after v0.9 release); final opportunity to give feedback before arxiv upload on September 1st, 2025. Give feedback here.
• May 12, 2025: version 0.9 of the preprint released; open feedback period until June 30, 2025.

📎 Pre-Preprint v0.99 Release, PDF Link
📎 Diff between v0.99 and v0.9, PDF Link
🚧 Live version of the manuscript (<- includes continuously integrated feedback such as typo corrections etc.)
🔍 Live diff with v0.99

Temporary BibTeX entry

@misc{bbchallenge_bb5,
  title  = {{Determination of the fifth Busy Beaver value}},
  author = {{The bbchallenge Collaboration} and Justin Blanchard and Dan Briggs and Konrad Deka and Nathan Fenner and Yannick Forster and Georgi Georgiev (Skelet) and Matthew L. House and Rachel Hunter and Iijil and Maja K\k{a}dzio\l{ka} and Pavel Kropitz and Shawn Ligocki and mxdys and Mateusz Na\'{s}ciszewski and savask and Tristan St\'{e}rin and Chris Xu and Jason Yuen and Th\'{e}o Zimmermann},
  year   = {2025},
  url    = {https://github.com/bbchallenge/bbchallenge-paper},
  note   = {In preparation, \url{https://github.com/bbchallenge/bbchallenge-paper}}
}

— The bbchallenge Collaboration

🦫 🦫 🦫