At the Limits of Computability: AI Agents Autonomously Discover Busy Beaver Accelerations

Paper Overview

• Field: Machine Learning
• Authors: Marco Dos Santos, Vivek Veeriah, Alex Havrilla, Andrew Bolt, Goran Zuzic, Satinder Singh, Tom Zahavy
• Posted: 2026-10-19
• arXiv: 2610.22603

Summary

Recent AI breakthroughs in mathematics—from Olympiad medal-level performance to resolving long-standing open conjectures—have rapidly expanded the capabilities of automated systems. However, these successes mainly revolve around problems pre-defined by humans; how AI systems can autonomously discover mathematical structure and propose new questions remains unresolved. To push beyond static challenges, this paper explores the Busy Beaver (BB) domain: an uncomputable frontier that is naturally suited to continuous exploration. Since no algorithm can compute the Busy Beaver number \(\mathrm{BB}(n)\) for every \(n\), this domain provides a natural setting for mathematical conjecture and proof.

The authors build a Gemini-based agentic pipeline that automatically discovers "accelerations" of Turing machines—compact mathematical rules summarizing large numbers of execution steps. The system 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 11 machines in \(\mathrm{BB}(6)\). Subject to community acceptance, these machines are provisionally classified as "Cryptids": machines whose blank-tape executions admit exact, compact mathematical descriptions, but whose halting behavior remains unresolved. The results advance the analysis of BB(6) holdouts and demonstrate the potential of autonomous AI systems for open-ended mathematical discovery in fundamental computer science.

Original 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.