With fifth busy beaver, researchers approach computation's limits

Original Article ↗ Hacker News Discussion ↗

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.