At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier

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, because these benchmarks primarily target fixed, human-formulated problems, they raise a provocative question: could AI systems eventually exhaust the supply of known mathematical questions? To push beyond static challenges, we explore the Busy Beaver (BB) domain, an uncomputable frontier that is fundamentally open-ended. Because no general algorithm can compute the sequence of Busy Beaver numbers for all 𝑛, making advances on this uncomputable frontier likely demands the invention of entirely new mathematical techniques. In this paper, we introduce a novel, Gemini-based agentic pipeline designed to automatically find accelerations of Turing machines: a common technique used when classifying machine halting behavior. 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 five machines. 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 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.