Determination of the Fifth Busy Beaver Value Authors: The bbchallenge Collaboration, including Justin Blanchard, Daniel 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. Submitted: 15 Sep 2025 Subjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL); Logic (math.LO) Pages: 48 pages, 17 figures DOI: 10.48550/arXiv.2509.12337 License: CC BY 4.0 (Creative Commons) --- Abstract The paper proves that the fifth Busy Beaver value, \( S(5) \), is 47,176,870. The Busy Beaver function \( S(n) \) is defined as the maximum number of steps an \( n \)-state 2-symbol Turing machine can run on a blank tape before halting. Introduced by Tibor Radó in 1962, \( S \) is a canonical example of an uncomputable function. The proof involves enumerating 181,385,789 5-state Turing machines and deciding exhaustively which machines halt. This marked the first new Busy Beaver value determined in over 40 years. It is also the first Busy Beaver value to be formally verified in a proof assistant (Coq). The work demonstrates the power of massively collaborative online research facilitated by the bbchallenge.org project. --- Technical Details and Contributions Uses formal verification in the Coq proof assistant to ensure correctness. Decides halting of a massive enumerated set of Turing machines by automated techniques. Provides significant progress in understanding an important uncomputable function in theoretical computer science. Details and the full proof span 48 pages and include 17 illustrative figures. --- Access PDF: Direct PDF Download HTML (experimental): View HTML TeX Source available for download. --- Additional Information Mathematical Subject Classification: Primary: 03D10 (Computability and recursion theory), 03B35 (Mechanics of proof, proof-theoretic semantics) Secondary: 68Q05 (Models of computation), 68Q45 (Formal languages and automata) ACM Classification: F.1.1 (Computability), F.4.1 (Mathematical Logic), I.2.3 (Deduction and Theorem Proving), D.2.4 (Software/Program Verification), F.4.3 (Formal Languages). --- Collaborative Nature and Impact The bbchallenge.org community combined expertise and computational resources to tackle a historically difficult problem. This work sets a new milestone in verifying properties of Turing machines and computability theory. Validates the effectiveness of proof assistants for large-scale mathematical and computer science results. --- Related Resources and Tools Bibliographic tools, citation exporters, and related papers are available on the hosting page. Additional services link to code, data, and demos tied to the paper. The project can serve as a foundation for exploring the implications of Busy Beaver values in computability and complexity theory. --- This achievement is a landmark advancement in the theoretical computer science domain, combining collaboration, computational enumeration, and formal proof verification to extend our understanding of the Busy Beaver function.