BB(5) = 47,176,870
We are extremely happy to announce that, after two years of intense collaboration, the goal of the Busy Beaver Challenge has been reached: the conjecture “BB(5) = 47,176,870” is proved. Exceeding our expectations, the proof has been formally written in Coq by collaborator mxdys whose work improves on and/or uses the contributions of more than 10 other bbchallenge contributors (see credits).
The formal theorem’s statement was reviewed by independent Coq experts (see credits) who confirmed that it indeed corresponds to “BB(5) = 47,176,870”. Furthermore, the Coq proof compiles correctly (in roughly 10 hours on a standard laptop), which implies that Coq believes the statement is true.
The proof enumerates the space of 5-state Turing machines (reduced to ~180 million machines using some symmetries) and runs custom algorithms, called deciders, that decide whether or not the machines halt from blank tape based on recognising specific behaviours. A handful of machines are proven individually, including the hard Skelet’s machines: #1 and #17.
This proof, which is the product of a massive collaborative effort ends a ~60 years long quest whose highlights are:
- 1962: Radó defines the “busy beaver game” and introduces functions S and Σ (we use BB = S, which is historically ambiguous)
- 1964: Green proves BB(5) ≥ 79
- 1984: the Dortmund contest is organised, Schult wins by proving BB(5) ≥ 134,467
- 1989: Marxen and Buntrock prove BB(5) ≥ 47,176,870
- 2003: Georgi Georgiev (Skelet) publishes a program that claims to decide all 5-state Turing machines but 43, Skelet’s 43 holdouts
- 2020: Scott Aaronson formally conjectures that BB(5) = 47,176,870
- 2022: The Busy Beaver Challenge (bbchallenge) is born, with the aim of collaboratively proving BB(5) = 47,176,870
- 2024: Coq-BB5 is published by bbchallenge contributor mxdys, achieving the challenge’s goal
See Pascal Michel’s website for more historical busy beaver information.
What’s next?
-
Human-readable paper. While the Coq proof settles the BB(5) quest, we are currently working on a human-readable paper that will explain the techniques that we used to decide 5-state Turing machines. We aim to have this paper published in the next two years both on arxiv and in recognised computer science venues.
-
Attacking BB(6) and multi-symbol. We are working on extending bbchallenge’s collaborative research platform to BB(6) and on multi-symbol busy beaver values such as BB(2,5) and BB(3,3). These busy beaver values currently correspond to the frontier of busy beaver knowledge (see our wiki) but mathematically-hard machines (called Cryptids) have already been found in each of these classes of machines. Notably, Antihydra is a 6-state 2-symbol machine whose behavior relates to the notoriously hard Collatz conjecture.
-
Developing, spreading and maintaining busy beaver knowledge. We aim at continuing developing bbchallenge as a space for collaborating on busy beaver problems, notably through our Discord server, forum, and recently created wiki.
Join us!!
The collaborative nature of the Busy Beaver Challenge has been a phenomenal catalyst for proving “BB(5) = 47,176,870”. With BB(6), BB(2,5) and BB(3,3), we are entering a new phase trying to tackle many more difficulties than we did up to now.
So, if you feel attracted to the busy beaver quest, we absolutely need your help!! Joining our Discord server is the easiest way to get started!
Credits
The following contributions were key to prove “BB(5) = 47,176,870”:
- mxdys for Coq-BB5
- Nathan Fenner for n-gram CPS, based on Skelet’s CPS, reverse engineered by savask
- Justin Blanchard, Mateusz Naściszewski (Mateon1), Konrad Deka (djmati1111) for Finite Automata Reduction (FAR)
- Iijil for Meet-in-the-Middle Weighted FAR (MITMWFAR)
- mei for busycoq, providing Coq proofs for various sets of machines
- Shawn Ligocki, mei and Jason Yuen for Shift Overflow counter
- Shawn Ligocki & Pavel Kropitz for Skelet 1, mei for the Coq proof
- Chris Xu for initial proof strategy of Skelet 17, mxdys for Coq proof
- Shawn Ligocki and Dan Briggs for Skelet 10 and mei for the Coq proof
- Justin Blanchard for “Finned machines” and mei for the Coq proof
bbchallenge’s maintainers have put in time and effort to have bbchallenge as a lively space for busy beaver research:
- Justin Blanchard (UncombedCoconut)
- Pavel Kropitz (uni)
- Shawn Ligocki
- mei
- Tristan Stérin (cosmo)
The following Coq experts confirmed the validity of the “BB(5) = 47,176,870” Coq statement:
Many thanks to the wider team of active bbchallenge contributors for their work and involvement in this research.
Very special thanks to Quanta magazine’s staff writer Ben Brubaker and his team for the time and effort they’ve spent researching and narrating our story:
Thank you all for this incredible journey, I’m really looking forward to seeing what comes next!
