Google DeepMind's Gemini finds eleven Busy Beaver Cryptids and proves them in Lean

What Google DeepMind published

Google DeepMind researchers have posted a paper describing a Gemini-based agent pipeline that found and formally verified new mathematical shortcuts for eleven previously unanalyzed six-state Turing machines on the Busy Beaver frontier. The paper, At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier (arXiv 2610.22603), was submitted on 15 October 2026. The authors are Marco Dos Santos, Vivek Veeriah, Alex Havrilla, Andrew Bolt, Goran Zuzic, Satinder Singh and Tom Zahavy, with Dos Santos also affiliated with the University of Cambridge while working at DeepMind.

The system discovers "accelerations": compact Collatz-like transition rules that summarize many low-level Turing-machine steps, then proves those rules in Lean 4. For the eleven machines, the authors say the blank-tape run is exactly described by such a system, so the machine halts if and only if the arithmetic system reaches a halt configuration. They provisionally call these machines Cryptids, subject to acceptance by the Busy Beaver Challenge community.

Proofs and related formalizations are in the public google-deepmind/cryptids repository under Apache-2.0 for code and CC BY 4.0 for other materials. That repository also holds separate, earlier Lean work that shrinks conjecture-checking machines for Goldbach, ZF consistency and the Riemann hypothesis; this article focuses on the Busy Beaver discoveries in the 15 October paper.

What the Busy Beaver problem is

The Busy Beaver function BB(n) asks how many steps the longest-running n-state, 2-symbol Turing machine can take before it halts, starting from a blank tape. Knowing BB(n) would decide the halting problem for every n-state machine: anything that runs past BB(n) steps never stops. That makes BB(n) uncomputable, and the sequence grows faster than any computable sequence.

The community has pinned down BB(2) through BB(5); BB(5) is 47,176,870, established by a large collaborative effort. The open frontiers include BB(6), BB(2,5) and BB(3,3). As of the paper's August 2026 snapshot, BB(6) still had about 1,094 holdouts after automated deciders, of which 18 were already treated as Cryptids. A Cryptid, in the authors' working definition, is a holdout whose blank-tape behaviour has an exact compact mathematical description whose halt-or-not question remains unresolved — often a Collatz-like map.

Progress on Busy Beaver is tracked on the Busy Beaver Challenge wiki. The DeepMind paper does not claim to have resolved BB(6); it claims to have produced verified accelerations that turn some holdouts into Cryptid-style arithmetic questions the community can attack next.

How the Gemini pipeline works

The pipeline has four stages. First, a custom simulator runs a machine for millions of steps and a compression algorithm turns tape contents into blocks of repeated symbols, ranking the most common abstract patterns. Second, Gemini 3.1 Pro conjectures Python transition rules over those patterns and refines them with an interactive simulator that can test synthetic configurations the blank-tape run may never hit. Third, the same model drafts informal proofs in a generator-evaluator loop. Fourth, a multi-persona Lean agent formalizes and compiles the proofs, with a critic that rejects vacuous or incomplete statements.

Only conjectures that predict 100 percent of recorded transitions advance to informal proving, and only evaluator-approved proofs go to Lean. The authors stress that the Lean stage may refine rule statements (for example by adding missing bounds) rather than treat the informal English as a rigid specification, because hand-wavy informal math often fails type checking.

Implementation details in the paper include simulating each machine for five million steps, taking the top 100 patterns, up to five interactive refinement turns, and a Lean agent time limit of 72 hours. A second stage later used a general-purpose auto-research agent with Gemini 3.8 Flash on remaining suspects, which the authors mark with a star in their results table.

Eleven new Cryptids, and fifteen rediscoveries

Table 1 of the paper lists eleven BB(6) machines as new discoveries: full accelerations and proofs for machines that, according to the authors, had no comparable documented analysis. Fifteen further machines are rediscoveries: formal proofs of rules similar to ones the community had already conjectured on Discord or the wiki, sometimes with higher-level accelerations.

Across the broad search the pipeline flagged 52 candidate machines with strong empirical rules, 50 of them in BB(6). The verified new Cryptids are a subset of that list. The authors explicitly say community acceptance still matters: their Cryptid label is provisional, and some community definitions require the underlying math problem to be recognised as genuinely hard.

None of these results by themselves decide whether the machines halt. An acceleration replaces millions of raw steps with a short system of arithmetic rules; whether that system ever hits halt can still be open — just as the Collatz conjecture remains open despite a one-line description.

The proofs live in Lean on GitHub

The cryptids GitHub repository packages Busy Beaver holdout proofs under a BusyBeaver/ Lean library, with kernel-checked behavioural theorems and a bridge to a separate ConjectureMachines layer. The README says proofs compile without sorry and depend only on the standard Lean axioms. Build instructions use Mathlib cache and a comparator audit configuration for Busy Beaver targets.

That matters because remote claims of "AI proved X" have a recent failure mode: papers and Lean repos that do not match. Keeping the machine definitions, start configurations and closure theorems in a public repository lets others replay the proofs rather than trust a blog summary.

Readers following Lean-assisted discovery will recognise the pattern from other October work, including Lean 4.35's "con leche" proof checker that Claude wrote and proved consistent and the still-disputed OpenAI Navier–Stokes Lean package, where mismatches between prose and code became the story. DeepMind's Busy Beaver release is closer to the first kind: the artefact is the proof.

How this fits other AI-for-math work

The paper situates itself against AI systems that solve human-posed contest problems or assist theory building, arguing Busy Beaver is a generator of open-ended questions no algorithm can finish. That is a different bet from Sakana's Agentic Scientist / AI Scientist v3, which automates machine-learning research loops, or from Anthropic's Claude Mythos 5 quantum-circuit designs, which optimises known engineering objectives.

Related DeepMind work in the same repository — not the main claim of the 15 October paper — certifies smaller Turing machines whose halting is equivalent to the failure of Goldbach, of ZF consistency, or of the Riemann hypothesis. Those reductions make the machines shorter; they do not resolve the conjectures. The Busy Beaver pipeline, by contrast, invents new dynamical descriptions for holdouts rather than encoding famous open problems.

The authors are frank that their current system targets Collatz-like structure. A more open-ended version would have to invent other classes of open problems, not only accelerate Collatz-like ones.

Limits and what is still open

Several caveats are in the paper itself. The Cryptid label is provisional. Some rediscoveries were not hand-checked by the authors against Discord history. Benefit varies by machine, and many BB(6) holdouts remain untouched. The pipeline is expensive: multi-hour Lean runs and millions of simulated steps per machine.

Independent readers still need to audit that each Lean statement matches the intended machine, that the blank-tape start configuration is correctly simulated, and that the closure of the rule system is genuine. The repository's comparator checks help, but they do not replace domain expertise from the Busy Beaver community.

Finally, an acceleration is not a non-halting proof. Turning Cryptids into resolved holdouts — or into accepted open problems with the status of Collatz — is future work for mathematicians and for later agents.

Why it matters

If the Lean proofs hold up under community review, DeepMind has shown a concrete loop for open-ended discovery at the edge of computability: simulate, conjecture, critique, formalise. That is rarer than another leaderboard score, and it produces artefacts other researchers can check.

For AI Lookout readers, the practical takeaway is narrower. When a lab claims an AI system discovered new mathematics, ask for the formal artefact, the exact statement proved, and what remains open. On this release, the artefact is public, the statements are accelerations and Cryptid classifications, and BB(6) itself is still unsolved.