ArXiv preprint (v2)

We've released the v2 of our paper on arXiv, see:

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

Changelog:

• Hydra definition typo in Conjecture 1.1 corrected: 3(x-1)/2 -> (3x-1)/2
• Abstract slightly reshaped
• Conceptual typos, mainly in loops, corrected
• State-of-the-art updated (holdouts: S(6), S(2,5), S(3,3), ZF)
• Some sentences were simplified
• Some bibtex references were updated (e.g. Equational Theories Project, now pointing to their arXiv paper)
• Re-layout of the author contribution Appendix and new people in Acknowledgement

We're thankful to the STOC 2026 Automated Pre-Submission Feedback which found most of the typos that we corrected in this v2.

ArXiv preprint (v1)

We've released the paper to arxiv, see:

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

🦫 Pre-Preprint Release (v0.99)

Feedback received during the open feedback period (May 12, 2025 to June 30, 2025) was integrated.

This is the last release of the pre-preprint before arxiv upload scheduled on September 1st, 2025. This is the final opportunity to give feedback before preprint release: give feedback here.

We attach to this release the diff PDF between v0.9 and v0.99, highlighting almost all the changes (a small set of changes do not appear, such as changes to the bibliography).

Changelog

• General: many typos fixed and grammatical uniformisation (thanks to @danbriggs and many others), BB(6) bound was updated
• Incipit: changed the two initial quotes from figure to epigraph
• Introduction: added mention of Abstract Interpretation; transformed some links into citations; paragraph "Coq and Coq-BB5" was largely reworked into "Proof assistants, Coq, and Coq-BB5"; more mentions to AI added in the discussion section; communities Googology and ConwayLife mentioned; added open 5-state machines questions to Future Work; S(6) prediction joke was made more explicit.
• Turing Machines: made step count convention more explicit
• Subsub sections "Pipelines" and "Deciders overview" promoted to subsections
• Loops: many mathematical typos were corrected; errors in pseudocode corrected
• NGramCP; RepWL; FAR: minor improvements
• WFAR: Bellman-Ford sentence expanded (and reference to LLM removed as it had been previously discovered by Justin Blanchard); definition of "weighted forward closed" corrected as per Iijil comment
• Bibliography: harmonised; capitalisation errors corrected
• Appendices: missing appendices filled in and minor moving around things/renaming

🦫 Pre-Preprint Release (v0.9)

🦫 Pre-Preprint Release — Determination of the fifth Busy Beaver value (v0.9)

We are proud to release the pre-preprint version of our paper:

🧾 Determination of the fifth Busy Beaver value

By:

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

📅 May 12, 2025

👉 Download Pre-Preprint (v0.9) PDF: bb5-pre-preprint-v0.9.pdf
🚧 Live version of the manuscript (<- includes continuously integrated Pre-Preprint feedback such as typo corrections etc.)
🔍 PDF showing difference between live manuscript and Pre-Preprint

🔍 About This Release

We prove that $S(5) = 47,176,870$ using the Coq proof assistant. This paper is serves as the official "human readable" version of the Coq proof of $S(5) = 47,176,870$: Coq-BB5.

This marks:

• The first new Busy Beaver value proven in over 40 years
• The first ever formally verified Busy Beaver value
• The culmination of a 2-year massively collaborative research effort at bbchallenge.org

This version is not yet submitted to any journal or preprint server. We are launching a 1.5-month open review phase (deadline: June 30st 2025) to gather feedback from co-authors, contributors, and the wider theoretical CS / logic / maths / formal methods communities.

---

📬 Want to Review or Suggest Improvements?

Start here → 🦫 Pre-Preprint Feedback Hub

You can:

• 📝 Comment on GitHub issues by section

• 🛠 Submit PRs for typos, clarifications, or suggestions

• ✉️ Send feedback via Google Form or email: feedback@bbchallenge.org

Review period ends June 30, 2025.

---

🙏 Acknowledgements

This release includes contributions from over 20 co-authors and hundreds of community members. The Coq formalisation, "Coq-BB5", embeds years of prior collaborative work from bbchallenge.org — including deciders, seed databases, and manual analyses.

Special thanks to all contributors past and present — your curiosity, persistence, and openness made this happen.

---

Let us know what you think — and help us make the final version even better 🚀

— The bbchallenge Collaboration

🦫 🦫 🦫