[July 2nd 2024] We have proved "BB(5) = 47,176,870"

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:

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”:

bbchallenge’s maintainers have put in time and effort to have bbchallenge as a lively space for busy beaver research:

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!

:beaver: :beaver: :beaver:

4 Likes