Prove that the 6-state Busy Beaver cryptid Antihydra never halts
Difficulty 84: halting is a Collatz-type statement about the parity of an iterated ⌊3n/2⌋ + 2 map, tied to Mahler's 3/2 problem, where no proof technique exists; placed above Hadwiger–Nelson (79) and Lehmer's totient problem (74), below Goldbach (92). Application value 1.5: none. Leverage 25: it gates any determination of BB(6) and would be a first proof for a Collatz-like dynamical system.
The problem
Prove that a specific six-rule Turing machine, Antihydra, runs for ever, as everyone expects but nobody can show.
- 1Six rules start a counting game
- 2Odd and even tallies wander randomly
- 3Halting needs a rare excursion
- 4Proof needs equidistribution results
The machine. Antihydra is a Turing machine with six states and two symbols: a tape of 0s and 1s, a read/write head, and a rule table with one "halt" entry. Its table, 1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA, can be simulated in a few lines of Python. Started on a blank tape, does it ever reach the halt rule?
What it is really computing. People on the bbchallenge project found that, after a short start-up, the machine's tape encodes two numbers and and each long pass of the head performs one step of a simple map:
Path to understanding
foundations → problemThe research entries this problem rests on, in the order to read them. Each links to its explainer.
- Start with
- Step 2
- Step 3
- Busy Beaver values and the bbchallenge projectTheory · host
- Then
- Prove that the 6-state Busy Beaver cryptid Antihydra never haltsThe problem
State of the art
The bbchallenge wiki gives only a probabilistic argument: the trajectory resembles a random walk with steps +2 or −1 of equal probability, which strongly suggests that Antihydra runs forever, but no proof exists. The wiki links the question to Mahler's Z-number problem, which needs equidistribution of {ξ(3/2)^n} on (0,1), described as a long-standing open question. Ligocki (2024) argues that any determination of BB(6) must decide Antihydra. The five-state case was resolved and formalised in Coq (arXiv:2509.12337), but that proof has no counterpart for 6-state cryptids. On the formal side, the reduction from the machine to the iteration above has been written in Lean 4 (rwst/Antihydra-Basics, lemma antihydra_halts_iff, generated mostly by language models and not independently reviewed); the open part is purely the number-theoretic statement.
Realistic applications
No practical application. Solving it would remove a main obstacle to BB(6) and would be a rare example of a formal proof for a Collatz-like dynamical system.
What counts as solved
A machine-checked proof (Lean 4, with Mathlib's Turing machine definitions or a self-contained model validated against the bbchallenge simulator) that Antihydra never halts, or a halting run proved by an explicit step count. The Lean source must compile with the three standard axioms only.
How it gets verified
Lean proofA formal proof checked by Lean 4 / Mathlib.
Route: Lean 4 + Mathlib, compiled with lake build and #print axioms showing only propext, Classical.choice and Quot.sound. The machine model must be cross-checked against the bbchallenge simulator on the first steps. An existing (unreviewed, not compiled by DARC) Lean development, rwst/Antihydra-Basics (Lean v4.29.0-rc6), defines the transition table, a zipper-tape run, and proves antihydra_halts_iff : (∃ k, (run initConfig k).state = none) ↔ ∃ i, (Aiter i (8, 2)).1 % 2 = 1 ∧ (Aiter i (8, 2)).1 / 2 ≥ 1 ∧ (Aiter i (8, 2)).2 = 0. Target statement (sketch against that model):
theorem antihydra_never_halts : ¬ ∃ k, (Antihydra.run Antihydra.initConfig k).state = none
A proof via the reduction must also be checked to be sorry-free end to end. Mathlib has general Turing machine models (Mathlib/Computability/TuringMachine/) but nothing specific to this machine; the BB(5) proof (ccz181078/Coq-BB5) is in Coq.
Claims under verification
+ add a claimNo claimed results on the Verification board for this problem yet.
Where the work is
A proof would need new mathematics about the equidistribution of fractional parts of (3/2)^n type sequences; computation can only run the machine further.
Bottlenecks
ranked by votes- #1TheoryEquidistribution of {ξ(3/2)^n}
Halting is tied to the parity statistics of an iterated ⌊3n/2⌋ + 2 map, a relative of Mahler's 3/2 problem; no known technique controls these fractional parts well enough to rule out a rare long excursion.
Community grades
Sign in to add your own grade.
Connected problems
No connections yet.
Progress
- Jul 6, 2024Antihydra analysedsource
Ligocki described why BB(6) is hard and the role of Antihydra.