At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier
Marco Dos Santos, Vivek Veeriah, Satinder Singh, Tom Zahavy and colleagues at Google DeepMind build a Gemini-based agentic pipeline that searches the Busy Beaver BB(6) frontier for compact mathematical rules describing Turing machine executions, and it discovered and formally verified Collatz-like accelerations for eleven previously unresolved machines.
Ask this paper
Why Busy Beaver. BB(n) is uncomputable, so no algorithm settles every machine. The domain has no fixed problem list, which makes it a test of whether an AI system can choose its own questions instead of solving human-posed ones.
Pipeline. The system chains pattern recognition over execution traces, automated conjecturing of acceleration rules, informal mathematical reasoning, and formal proof in Lean. A rule summarizes many execution steps in one closed-form update.
Result. It produced Lean-verified accelerations for eleven BB(6) holdout machines. The authors provisionally classify them as Cryptids: their blank-tape runs have exact compact descriptions, but whether they halt is still open.
Verification as the gate. Every accepted rule is a Lean proof, so the output does not depend on trusting the model's informal reasoning. This is the same design choice that made recent olympiad and conjecture results credible.
Why it matters. It is one of the few demonstrations of an agent producing new, formally checked mathematical objects in an open-ended domain, rather than answering a fixed benchmark.
Abstract
Recent breakthroughs in AI for mathematics---ranging from Olympiad medal performances to resolving long-standing open conjectures---have rapidly expanded what automated systems can achieve. Yet these successes primarily concern predefined, human-formulated problems, leaving open how AI systems can autonomously uncover mathematical structure and formulate new questions. To push beyond static challenges, we explore the Busy Beaver (BB) domain, an uncomputable frontier that is fundamentally open-ended. Because no algorithm can compute the Busy Beaver number $\mathrm{BB}(n)$ for every $n$, this domain provides a natural setting for sustained exploration through mathematical conjecture and proof. In this paper, we introduce a Gemini-based agentic pipeline that automatically discovers accelerations of Turing machines, expressed as compact mathematical rules summarizing many execution steps. Our system integrates pattern recognition, automated conjecturing, informal mathematical reasoning, and formal theorem proving in Lean. With this framework, our system autonomously discovered and formally verified novel Collatz-like accelerations for eleven machines in $\mathrm{BB}(6)$. Subject to community acceptance, we provisionally classify these machines as Cryptids, namely machines whose blank-tape executions admit exact, compact mathematical descriptions but whose halting behavior remains unresolved. These results advance the analysis of $\mathrm{BB}(6)$ holdouts on the Busy Beaver frontier and demonstrate the potential of autonomous AI systems for open-ended mathematical discovery in fundamental computer science.