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 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 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 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
BB(6)
Full
-
1RB1RD_0LC1RA_0RA1LC_1RA1LE_1RF0LD_---0RE
BB(6)
Full
† .
1RB1RB_1LC0RE_---1LD_0RA1LB_1RA1LF_0LE1LE
BB(6)
Full
†
1RB0LF_1LC1RA_0RE0RD_---1LE_1LF1RC_1LC1LA
BB(6)
Full
†
1RB1RD_0LC1RA_1RA1LC_0RB1LE_1RF0LD_---0RE
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 † 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 ‡ rediscoveries that were formally proved by our system but we did not check by hand. We label machines with ⋆ 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.
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.
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).
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.
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.
Stephen Chung, Wenyu Du, William J. Wesley
DualverseAI · University of Cambridge · University of Hong Kong +1
We introduce the AI co-mathematician, a workbench for mathematicians to interactively leverage AI agents to pursue open-ended research. The AI co-mathematician is optimized to provide holistic support for the exploratory and iterative reality of mathematical workflows, including ideation, literature search, computational exploration, theorem proving and theory building. By providing an asynchronous, stateful workspace that manages uncertainty, refines user intent, tracks failed hypotheses, and outputs native mathematical artifacts, the system mirrors human collaborative workflows. In early tests, the AI co-mathematician helped researchers solve open problems, identify new research directions, and uncover overlooked literature references. Besides demonstrating a highly interactive paradigm for AI-assisted mathematical discovery, the AI co-mathematician also achieves state of the art results on hard problem-solving benchmarks, including scoring 48% on FrontierMath Tier 4, a new high score among all AI systems evaluated.
Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to generate formal proofs in languages like Lean. We perform the first large-scale evaluation of this method's ability to solve open problems. Our most capable agent autonomously resolved 9 of 353 open Erdős problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes but proved costlier on the hardest problems. These findings demonstrate the power of AI-aided formal proof search and shed light on the agent designs that enable it.
George Tsoukalas, Anton Kovsharov, Sergey Shirobokov +18