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

Marco Dos Santos; Vivek Veeriah; Alex Havrilla; Andrew Bolt; Goran Zuzic; Satinder Singh; Tom Zahavy

cs.AIOct 15, 2026

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

Authors: Marco Dos Santos, Vivek Veeriah, Alex Havrilla, Andrew Bolt, Goran Zuzic, Satinder Singh, Tom Zahavy

Organizations: Google DeepMind · University of Cambridge

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.

Figures & tables

Machine	BB domain	Discovery type	Comment
Part I: New Discoveries
1RB1LD_1RC0RA_1LA1RE_0LA0LB_0RB1RF_---1RD	$\mathrm{BB}(6)$	Full	-
1RB1RD_0LC1RA_0RA1LC_1RA1LE_1RF0LD_---0RE	$\mathrm{BB}(6)$	Full	$\dagger$ .
1RB1RB_1LC0RE_---1LD_0RA1LB_1RA1LF_0LE1LE	$\mathrm{BB}(6)$	Full	$\dagger$
1RB0LF_1LC1RA_0RE0RD_---1LE_1LF1RC_1LC1LA	$\mathrm{BB}(6)$	Full	$\dagger$
1RB1RD_0LC1RA_1RA1LC_0RB1LE_1RF0LD_---0RE	$\mathrm{BB}(6)$	Full	†⋆

Table 1: Collatz-like accelerations discovered by our system. We distinguish three discovery types. Full: new acceleration and proof. Acceleration: new acceleration for a known machine, with its proof. Proof: formal proof of rules similar to known ones. Appendix B provides a detailed comparison between our rule systems and those previously proposed by the community. For machines with known or suspected accelerations, we cite the original source and highlight the added value of our analysis, such as a formal proof or a higher-level acceleration. For previously unanalyzed machines, our results represent complete, novel discoveries. We label machines with

\dagger

if they were mentioned in a Discord message by dyuan01 as holdouts with a high "complexity score", but with no rules or analysis, and with

\ddagger

rediscoveries that were formally proved by our system but we did not check by hand. We label machines with

\star

if they were discovered in a second stage of our pipeline. Specifically, following the completion of the full pipeline, we used a general-purpose auto-research system equipped with the recent Gemini 3.8 Flash model, which had access to all the results and code in this paper. We tasked it to conjecture and prove the equivalence of all the remaining suspects. This system was granted the ability to selectively make progress on machines and was incentivized to find as many accelerations as possible, with more compressed accelerations earning higher point values. The prompt used for this second stage is provided in Appendix E .

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.

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Class	Meaning	#	Machines
Exact	Same configuration families and the same transitions as the published rules (up to renaming, additive parameterization, or a one-step head phase). Our contribution is the formal closure proof.	2	1RB1LE_1LC0RA_0RF0LD_1LE1LA_1RC0LB_---1RC 1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA (BMO 8)
Equivalent, reformulated	Same dynamics, but our families or acceleration level differ: typically we expose an extra sweep parameter, so each published rule is a composition (or a slice) of several of ours, and the community’s higher-level (exponential) formulations are not proved.	8	1RB0RF_1RC1RF_1LD0LE_---1LC_1RA1LE_1LC1RB 1RB1LC_1RC0LD_1LA0RB_1LB1LE_1RF0LA_---0RE (BMO 5, TNF C) 1RB1LC_1LC1RD_1LA0LB_0RB1RE_1RF0RA_---0RC 1RB1RE_1LC0RA_0RD1LB_---1RC_1LF1RE_0LB0LE (BMO 1) 1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE (BMO 5) 1RB1RE_1LC0RA_1RD0LB_1LB1RC_1LF0RD_---0LE (BMO 5, TNF D) 1RB3LA1LA1RA1RA_2LB2RA---4RB1LB (BB(2,5)) 1RB1RF_0LC0RF_1RD1LC_---0LE_0RC1LF_1RA0LE
Different decomposition	Genuinely different rule systems: the community has no closed system (a single partial rule, or closure conditional on an unproved number-theoretic inequality), or our proof sits at a different acceleration level (one-step CTL vs. macro rules).	3	1RB1LA_1RC1RE_1LD0RB_1LA0LC_0RF0RD_0RB--- 1RB1RF_1LC1LF_0RE1LD_0LB1LD_---1RC_1RA0RD 1RB---_0RC0RD_1LD1RB_0LE0LC_1RA0LF_1LD1LE
Undetermined	Community rules were only posted on Discord and we were not able to reproduce.	2	1RB0LE_1LC1RA_1RA1LD_0LC0LA_0RE1RF_0RC--- 1RB0RB_1LB0LC_1RD1LC_1RE0RA_0RF1RA_---1LB

Appendix

Table 3: Relation between the macro-rule systems we prove in Lean 4 and the rules previously published by the bbchallenge community (Wiki/Discord), for the 15 rediscovery machines. Correspondences were checked by direct simulation.

Autonomous Scientific Discovery

Autonomous scientific discovery develops AI systems that generate, test, and refine scientific hypotheses using data, computation, and experiments.

See all 128 papers

Autonomous Mathematical Discovery in an Open-World Multi-Agent Environment
Aug 24, 2026Stephen Chung, Wenyu Du, William J. WesleyMulti-Agent Collaboration Multi-Agent Systems
DualverseAI · University of Cambridge · University of Hong Kong +1
AI co-mathematician: Accelerating mathematicians with agentic AI
May 7, 2026Daniel Zheng, Ingrid von Glehn, Yori Zwols +15AI Agents for Scientific Discovery AI-Assisted Mathematical Discovery
Google DeepMind · Google
Advancing Mathematics Research with AI-Driven Formal Proof Search
May 21, 2026George Tsoukalas, Anton Kovsharov, Sergey Shirobokov +18Large Language Model-Guided Theorem Proving Automated Theorem Proving
1Google DeepMind1 · 2Aarhus University · 3Google

Aug 24, 2026J/K move · Enter open · S save

Autonomous Mathematical Discovery in an Open-World Multi-Agent Environment

Stephen Chung, Wenyu Du, William J. Wesley

DualverseAI · University of Cambridge · University of Hong Kong+1

Multi-Agent Collaboration Multi-Agent Systems Autonomous Scientific Discovery Autonomous Research Agents

Open paper AskPDF arXiv

We study autonomous mathematical discovery in the Station, an open-world multi-agent environment in which AI agents from different model families pursue a shared research goal without a central coordinator or scripted pipeline. Agents choose their own research directions, conduct experiments, collaborate and publish papers. These papers accumulate into a shared body of knowledge that later agents can read, cite and extend. We evaluated the Station on 12 mathematical construction problems from the AlphaEvolve study and two additional case studies. Five of the 12 problems yielded results novel relative to the prior literature: a new infinite family of finite field Kakeya sets, new exact 604-point kissing configurations in eleven dimensions, improved bounds for the discretized Kakeya needle and sign uncertainty problems, and a substantially improved lower bound for Erdős's minimum overlap problem. Agents also discovered novel infinite families for Book Ramsey numbers. Their research extended beyond searching for high-scoring constructions: agents developed explanations of their findings and proved theorems outside the assigned tasks. These explanations guided further discoveries and were preserved in the agents' papers, making the underlying insights easier for external researchers to understand and build upon. All presented discoveries are supported by exact constructions or proofs formally verified in Lean. We release the source code, full agent dialogues, papers and verification code, providing a transparent record of how these discoveries emerged.

Abstract

Autonomous Scientific Discovery

Explore similar work

Autonomous Mathematical Discovery in an Open-World Multi-Agent Environment

AI co-mathematician: Accelerating mathematicians with agentic AI

Advancing Mathematics Research with AI-Driven Formal Proof Search