Determination of the fifth Busy Beaver value

Original Article ↗ Hacker News Discussion ↗

How BB(5) Was Determined

  • Direct “run them all and see” is impossible because you can’t in general detect non-halting by brute force.
  • The search space of 5-state Turing machines was first reduced using Tree Normal Form, from ~1.7×10¹³ raw machines to ~1.8×10⁸ “essentially different” ones (reachable states canonically ordered, symmetries reduced).
  • Machines were then passed through a pipeline of deciders:
    • Simple loop detection (“loops”) plus short simulations handled the vast majority.
    • More sophisticated abstract-interpretation deciders (NGram CPS, RepWL, FAR, WFAR) proved non-halting for almost all remaining machines by over-approximating reachable configurations and showing none can reach a halting state.
    • Only 13 “sporadic” machines needed bespoke, hand-crafted non-halting proofs.
  • The longest halting machine runs for 47,176,870 steps, establishing BB(5).

Brute Force vs Uncomputability

  • Commenters stress that the Busy Beaver function as a whole is uncomputable, but specific small values (like BB(5)) can still be determined with enough structure and proof.
  • There is no universal algorithm deciding halting for all Turing machines (halting problem), but for any fixed finite class (e.g., up to 5 states) a specialized decider can exist.
  • Some argue that, in a broad sense, this is still “brute force”: enumerate machines and proofs within a formal system; others reply that the key work is in designing powerful deciders and proof strategies, not naive enumeration.

Limits of Proving Busy Beaver Values

  • For any fixed, sound, recursively axiomatizable theory, there exists some N beyond which that theory cannot prove exact BB(N) values; this is a Busy-Beaver-flavored incompleteness phenomenon.
  • One view: there is no absolute N beyond which BB(N) is unknowable “in principle”; you can always strengthen your axioms. Another view emphasizes that for every such theory, independence eventually occurs.
  • Known results (cited in the thread) show certain large BB(k) values (e.g., around k≈745) are already independent of ZFC; the suspected “practical” barrier might be much smaller, possibly even low double digits.

Proof Assistants and Rocq

  • All deciders and sporadic proofs were formalized in the Rocq (Coq) proof assistant.
  • This ensures the full BB(5) classification is machine-checked: deciders are proved correct with respect to mathematical Turing machines, then applied to the entire search space.
  • Verifying the resulting proof takes under an hour on a multi-core laptop; the exploratory search and development of deciders took far more computational and human effort.
  • There is discussion of alternative assistants (e.g., Lean, Dafny), and of this work as part of a broader trend toward formalized, collaborative mathematics.

Online Collaboration and Related Communities

  • The project is highlighted as a large, distributed, internet-native collaboration, closer to “formalized research” than distributed number-crunching.
  • Comparisons are made to:
    • Classic distributed projects (DES/RSA challenges, distributed.net), whose original goals are now largely historical.
    • Modern formal-math collaborations in Lean using proof “blueprints”.
    • Niche online communities around Conway’s Game of Life and “googology” (very large numbers).

Implications and Practical Value

  • Most participants see this as highly theoretical, with no direct applied payoff; benefits lie in:
    • Sharpened methods for reasoning about program behavior and partial halting-problem “taming” (e.g., static-analysis techniques, abstract interpretation).
    • Stress-testing and improving proof assistants and libraries.
    • Deepening understanding of the limits of formal systems and computability.
  • Some push back on the idea of “purely useless” math, citing historical cases where seemingly abstract work later became foundational (e.g., number theory, Hardy’s work).
  • Others characterize the achievement as more of a heroic, intricate classification effort than a new conceptual breakthrough—still “beautiful” and inspiring.

Connections to Collatz and BB(6)

  • The 5-state champion is described (elsewhere, and referenced here) as computing a Collatz-like process; commenters note similar behavior in candidate 6-state “Antihydra” machines.
  • This raises the idea that Collatz-style dynamics are a good blueprint for constructing long but terminating computations.
  • BB(6) is discussed only via bounds and scale:
    • Published lower bounds already involve mind-boggling fast-growing constructions (towers/Knuth arrows repeated enormous numbers of times).
    • An exact BB(6) is believed far beyond what can be written down or feasibly proved, even if not yet formally ruled out.