With fifth busy beaver, researchers approach computation's limits

Original Article ↗ Hacker News Discussion ↗

Researchers have finally pinned down the exact value of the 5‑state Busy Beaver function — the maximum running time of any 5‑state Turing machine on a blank tape — using a 19,000‑line proof in the Coq theorem prover. Commenters explore why this matters: it sharpens our understanding of the halting problem and uncomputability, shows how far formal verification and automated analysis can go on small machines, and highlights how quickly things become intractable, with the next case (6 states) already entangled with deep open problems like Collatz-type behavior and likely beyond current mathematics.

Definitions and conventions

  • Two main Busy Beaver functions discussed:
    • Σ(n): max number of 1s left on tape at halt.
    • S(n): max number of steps until halt.
  • Notation conflicts: some use BB(n) for steps, others for marks. Recent work and publicity tends to use BB = steps.
  • For 5-state, 2-symbol machines, current results: S(5) = 47,176,870 steps; Σ(5) = 4098 ones.

Nature of the BB(5) result and proof

  • The 5-state, 2-symbol blank-tape halting problem is now completely classified.
  • Proof is formalized in Coq (~19k lines). Earlier proofs and “deciders” existed but were fragmented and partly mistrusted.
  • Coq formalization tightened confidence, especially for tricky non-halting machines that needed bespoke acceleration or long manual reasoning.

Limits, undecidability, and BB(6)+

  • BB(6) is known to be at least absurdly large; a specific 6-state machine (“Antihydra”) behaves like a Collatz-type iteration and seems intractable without new mathematics.
  • Related 2-state, 5-symbol “Hydra” machine and Mahler-style distribution conjectures are mentioned as barriers.
  • General incompleteness results guarantee some BB(n) are unprovable in standard systems; concrete encodings give independence around n ≈ 700+, far above 5.
  • Debate over whether BB(6) or BB(7) could already encode undecidable behavior; many find that unlikely but not impossible.

Behavior and structure of champion machines

  • Observed output patterns for small champions often look fractal or self-similar (e.g., “bouncing” growth giving parabolic patterns).
  • Two conjectural trends:
    • “Spaghetti code” conjecture: larger champions become increasingly chaotic.
    • “Clean code” conjecture: winners might have simple, structured programs but implement exotic mathematics.
  • Some expect a mix of both; systematic trends might be too strong to be true, since they’d overly aid search.

Variants and combinatorics

  • Other formulations: counting steps vs marks, lambda-calculus / Kolmogorov-style busy beavers, multi-symbol variants (e.g., 2 states / 4 symbols).
  • Formula for number of n‑state, 2‑symbol TMs: (4(n+1))^(2n); with certain reductions, (4n+1)^(2n), giving ~17 trillion 5‑state machines.
  • Determining exact halting percentages for 5‑state machines is nontrivial due to normal forms and multiplicities; unclear in thread.

Philosophy and value

  • Some question practical payoff versus “more relevant” work.
  • Responses emphasize:
    • Intrinsic curiosity and personal fulfillment.
    • Historical pattern where abstract theory later gains applications.
    • Role of Busy Beaver as a clean window into computability, the halting problem, proof complexity, and limits of formal systems.
  • Discussion also touches on whether human insight could in principle transcend fixed formal systems for specific halting questions; views diverge.