Busy Beavers
A Gemini-based agent that studies unresolved six-state Turing machines, discovers compact Collatz-like rules for how they run, and proves those rules in Lean — including eleven machines nobody had analysed before.
1RB0LF_1LC1RA_0RE0RD_---1LE_1LF1RC_1LC1LA. Time runs left to right; each column is the tape. The striped blocks are the (10) and 1 runs that its acceleration rule tracks.The Busy Beaver number BB(n) is the longest any n-state Turing machine can run on a blank tape and still halt. The function is uncomputable, so every value has to be won by hand: you must settle every holdout machine, proving that it halts or that it runs forever. BB(5) was settled by the Busy Beaver Challenge community. In BB(6), some holdouts turn out to be Cryptids — machines whose behaviour reduces to a Collatz-like problem, so deciding whether they halt is as hard as an open question in number theory.
We built an agentic pipeline on Gemini that does this analysis end to end. It simulates a machine, compresses its tape into recurring patterns, conjectures an acceleration — a compact rule that jumps over many steps at once — tests the rule, writes an informal proof, and then proves it formally in Lean 4. Run across the BB(6) holdouts, it produced verified accelerations for eleven machines with no prior documented analysis, which we provisionally classify as new Cryptids pending community review, and formally re-derived the rules for fifteen machines the community had already studied.
Results
How it works
- 1
Find patterns
Simulate the machine for millions of steps, compress the tape into blocks, and group recurring configurations into abstract patterns.
- 2
Conjecture a rule
Gemini writes the transition rule between patterns as code, probes edge cases with an interactive simulator, and revises until the rule matches the machine.
- 3
Prove it informally
A generator–evaluator loop writes and critiques a mathematical proof that the rule is a faithful acceleration of the machine.
- 4
Prove it in Lean
A team of agents — setter, planner, writer, critic — turns the argument into a kernel-checked Lean 4 proof, building on BusyLean.
What an acceleration looks like
The machine pictured above writes a block of alternating 10 pairs followed by a run of 1s. Write C(a, b) for the moment the head sits in state E at the left edge of a copies of 10 and b ones. After seven steps the machine reaches C(0, 3), and from then on thousands of steps collapse into one rule:
| C(2a+2, b−2a−2) | if b > 2a+2 |
| C(2, 2a+2) | if b = 1 |
| Halt | if b = 2 |
| C(⌊n/4⌋, n mod 4 + 1) | if b = 2k, 2 ≤ k ≤ a+1, with n = 6a+2k+2 |
| C(⌊n/4⌋, n mod 4 + 1) | if b = 2k+1, 1 ≤ k ≤ a, with n = 6a+2k+6 |
Whether the machine ever halts is now a question about this map: does the orbit of C(0, 3) ever land on b = 2? The rule is proved to be an exact acceleration of the machine in Lean; the question it leaves behind has the flavour of the Collatz conjecture.
The proofs
All the Lean proofs are open source in google-deepmind/cryptids. Alongside the BB(6) machines from the paper, the repository covers all six remaining BB(3,3) holdouts, and a separate library of conjecture-checking machines — small Turing machines that halt if and only if Goldbach’s conjecture or the Riemann hypothesis fails, or ZF is inconsistent. Contributions from the Busy Beaver community are welcome.
Marco Dos Santos, Vivek Veeriah, Alex Havrilla, Andrew Bolt, Goran Zuzic, Satinder Singh, Tom Zahavy. Google DeepMind and the University of Cambridge, October 2026.