Determination of the fifth Busy Beaver value
Logic in Computer Science
2026-03-24 v2 Formal Languages and Automata Theory
Logic
Abstract
The Busy Beaver value is the maximum number of steps that an -state 2-symbol Turing machine can perform from the all-zero tape before halting. was historically introduced by Tibor Rad\'o in 1962 as one of the simplest examples of an uncomputable function. We prove that using the Coq proof assistant. The proof enumerates 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 (bbchallengeorg).
Cite
@article{arxiv.2509.12337,
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},
journal= {arXiv preprint arXiv:2509.12337},
year = {2026}
}
Comments
48 pages, 17 figures