Recent breakthroughs in AI for mathematics—ranging from Olympiad‑medal solutions to the resolution of long‑standing conjectures—have dramatically expanded what automated systems can achieve. However, these successes mainly address predefined, human‑crafted problems, leaving open the question of how AI can autonomously uncover mathematical structure and pose new questions.
The Busy Beaver (BB) problem is an uncomputable frontier: no algorithm can compute $\mathrm{BB}(n)$ for every $n$. This makes BB a natural, open‑ended arena for sustained exploration via conjecture and proof.
We introduce a Gemini‑based agentic pipeline that automatically discovers accelerations of Turing machines, expressed as compact mathematical rules summarizing many execution steps. The pipeline integrates pattern recognition, automated conjecturing, informal mathematical reasoning, and formal theorem proving in Lean.
Using this framework, the system autonomously discovered and formally verified novel Collatz‑like accelerations for eleven machines in $\mathrm{BB}(6)$. These machines admit exact, concise mathematical descriptions of their blank‑tape executions, yet their halting behavior remains unresolved.
We provisionally label such machines "Cryptids"—machines whose executions can be precisely described but whose termination status is unknown. This classification helps organize the remaining challenges of $\mathrm{BB}(6)$ and provides clear targets for future work.
The results demonstrate the potential of autonomous AI systems for open‑ended mathematical discovery in fundamental computer science, marking a shift from static challenges to dynamic exploration.
Review