🦫 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).

ArXiv Preprint (v1)

The paper has been released to ArXiv on September 15th, 2025:

📄 https://arxiv.org/abs/2509.12337

The paper may receive further corrections on this repository, see:

🚧 Live version of the manuscript

Citing this work

Currently, please use the following two bibtex entries:

@misc{BB5,
      title={{Determination of the fifth Busy Beaver value}}, 
      author={{The bbchallenge Collaboration} and Justin Blanchard and Daniel Briggs and Konrad Deka and Nathan Fenner and Yannick Forster and Georgi Georgiev and Matthew L. House and Rachel Hunter and Iijil and Maja Kądziołka and Pavel Kropitz and Shawn Ligocki and mxdys and Mateusz Naściszewski and savask and Tristan Stérin and Chris Xu and Jason Yuen and Théo Zimmermann},
      year={2025},
      eprint={2509.12337},
      archivePrefix={arXiv},
      primaryClass={cs.LO},
      url={https://arxiv.org/abs/2509.12337},
      note={\url{https://arxiv.org/abs/2509.12337}}
}

@software{mxdys_2025_17061968,
  author    = {mxdys},
  title     = {{Coq-BB5 release v1.0.0}},
  month     = sep,
  year      = 2025,
  publisher = {Zenodo},
  version   = {1.0.0},
  doi       = {10.5281/zenodo.17061968},
  url       = {https://doi.org/10.5281/zenodo.17061968},
  note      = {\url{https://doi.org/10.5281/zenodo.17061968}}
}

— The bbchallenge Collaboration

🦫 🦫 🦫