A Gemini agent proves conjectured Turing-machine acceleration rules as Lean 4 theorems, building on the BusyLean repository's Turing machine definitions.
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.
Problem
Most AI-for-mathematics successes target predefined, human-posed problems. The Busy Beaver domain is uncomputable and open-ended, which makes it a testbed for AI that discovers mathematical structure itself. Unresolved BB(6) holdout machines need compact, verified descriptions of how they behave.
Approach
A four-stage agentic pipeline built on Gemini 3.1 Pro. First, each Turing machine is simulated and its tape configurations are compressed into abstract patterns. An LLM then conjectures transition rules over these patterns and refines them with targeted simulations. Informal proofs are produced in a generator-evaluator loop and then translated by an agent into machine-checked Lean 4 theorems, building on the BusyLean repository.
Figure 1 : Overview of the automated discovery pipeline, detailing the progression from empirical pattern detection and LLM-guided rule conjecturing to informal proving and formal verification in Lean 4.
Results
The system discovered and formally verified novel Collatz-like accelerations for eleven BB(6) machines and also handled machines in the BB(2,5) domain. Subject to community acceptance, these BB(6) machines are provisionally classified as Cryptids. For several machines, the pipeline also proved rules the community had published earlier.
