PaperlayerView exact revision on arXiv

Source-linked AI summary

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

arXiv:2610.22603v2cs.AIcs.FL

TL;DR

AI mathematics has largely addressed predefined, human-formulated questions, leaving open how systems might discover mathematical structure and formulate new questions. The paper introduces a Gemini-based pipeline that derives and formally verifies Turing-machine accelerations. It reports novel, formally verified Collatz-like accelerations for eleven BB(6) machines, provisionally classifying them as Cryptids subject to community acceptance.

  • Problem

    AI mathematics has largely focused on predefined, human-formulated questions, leaving open how systems can autonomously uncover mathematical structure and formulate new questions.

    Source: §1 · p. 1

  • Method

    A Gemini-based pipeline compresses simulated machine behavior into mathematical rules and proves their equivalence in Lean.

    Source: §1 · p. 3, §6 · p. 10

  • Results

    Eleven BB(6) machines received novel, formally verified Collatz-like accelerations and were provisionally classified as Cryptids subject to community acceptance.

    Source: §1 · p. 3, §6 · p. 10

  • Takeaways & Limitations

    The results represent a step toward systematically classifying remaining Busy Beaver holdouts.

    Source: §6 · p. 10

    The current approach accelerates machines exhibiting Collatz-like functions and is not entirely open-ended.

    Source: §6 · p. 10

Abstract

from arXiv · show

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.

1. Introduction

The paper uses the Busy Beaver frontier to explore AI discovery beyond solving predefined questions. Its pipeline derives and formally verifies compact accelerations, including new Collatz-like rules for eleven BB(6) holdouts.

1. Introduction

  • The Busy Beaver frontier offers an open-ended setting for mathematical conjecture and proof because no algorithm computes BB(n) for every n.The paper frames this as a route toward AI contributing to mathematical structure discovery and new question formulation, beyond solving predefined, human-formulated problems.Source: §1 · p. 1
  • The study focuses on approximately 1,000 BB(6) holdouts, some of which have dynamics corresponding to open mathematical problems and remain unresolved.An acceleration summarizes many low-level machine steps in compact transition rules, potentially facilitating halting analysis or revealing a mapping to a Collatz-like system.Source: §1 · p. 3
  • A Gemini-based coding scientist compresses simulated execution into mathematical equations and proves their equivalence in Lean, treating machines as grey boxes rather than analyzing their transition rules statically.The pipeline detects patterns, conjectures transition rules, refines them through simulation, drafts informal proofs, and formally verifies them in Lean 4.Source: §1 · p. 3
  • For eleven previously unanalyzed BB(6) holdouts, the system proved exact Collatz-like descriptions of blank-tape execution, reducing each halting question to whether the corresponding system reaches a halting configuration.The authors provisionally classify these machines as Cryptids subject to community acceptance; they also report similar rules or new accelerations for fifteen previously studied machines.Source: §1 · p. 3

2. Background

The background defines the Busy Beaver problem and its unresolved holdouts, then introduces Cryptids as holdouts with compact mathematical descriptions but unresolved halting behavior. Their Collatz-like dynamics can accelerate simulation without resolving whether they halt.

2.1. Turing Machines and the Busy Beaver Problem

  • BB(n,m) is the maximum runtime of a halting n-state, m-symbol machine on a blank tape; resolving every holdout is necessary to determine the corresponding Busy Beaver value.For two-symbol machines the notation is BB(n); the passage lists BB(2) = 6, BB(3) = 21, BB(4) = 107, and BB(5) = 47,176,870.Source: §2.1 · p. 4

2.2. Cryptids and Collatz-like Systems

  • A Cryptid is a holdout whose blank-tape execution has an exact, compact dynamical description while whether its trajectory reaches a halting condition remains unresolved.The paper's definition is broader than conventional community usage, so its new Cryptid classifications remain subject to community acceptance.Source: §2.2 · p. 4
  • Collatz-like systems encode tape blocks with exponent parameters and use piecewise-affine updates selected by congruence classes, replacing many machine steps with one macro-transition.Simple rules do not make long-term behavior predictable; the passage notes that reachability is undecidable for a class of generalized Collatz maps.Source: §2.2 · p. 4
  • For Cryptids encountered in BB(6), proximity to a frontier of what ZFC can prove is speculative, while whether their trajectories halt remains an open problem.Unresolved trajectories obstruct completion of the corresponding Busy Beaver classifications.Source: §2.2 · p. 5
  • Antihydra reaches A(0, 4) after 11 steps, then follows exact macro-transitions; it halts if and only if its trajectory reaches A(0, 2b+1), which remains unknown.The state F corresponds to the halting case because the machine then reaches an undefined F0 transition.Source: §2.2 · p. 5

3. Method

The method moves from observed Turing-machine configurations to conjectured transition rules, then tests and proves those rules through informal reasoning and Lean verification.

3.1. Pattern Detection

  • Configurations are compressed into symbol blocks with exponents, abstracted as patterns without their specific exponents, and ranked by frequency to select dominant behaviors.A custom compression algorithm uses a simplicity score and one-step lookahead to parse tape blocks.Source: §3.1 · p. 5

3.2. Automated Conjecturing of Transition Rules

  • For frequent patterns, an LLM turns observed transitions into executable exponent-update rules that can be tested against the recorded data.The initial rules can miss edge cases absent from the observed execution trace.Source: §3.2 · pp. 5–6

3.3. Interactive Refinement of Conjectures

  • Interactive simulation lets the LLM probe chosen configurations, including cases unreachable from the blank-tape trajectory, and refine incomplete rules.After refinement, rules are expressed as piecewise mathematical functions and may be algebraically accelerated across multiple transitions.Source: §3.3 · pp. 6–7

3.4. Informal Proving

  • Each conjectured case must predict 100% of recorded transitions before entering an iterative generator-evaluator loop that revises informal proofs until both correctness and format scores reach 1.Accepted proofs are passed to Lean for formal verification.Source: §3.4 · p. 7

3.5. Formal Proving

  • The formal-proving process starts from Lean statements for equivalence, system closure, and the target halting or non-halting theorems.It terminates successfully when required theorems compile without unproven goals or unauthorized axioms, or unsuccessfully at the 72-hour limit.Source: §3.5 · pp. 7–8
  • The Lean agent may refine seeded statements to address missing bounds or rules; the Critic checks proofs and formalizations while feedback and simulations help correct errors.A successful system proves each rule against the fixed machine and is closed: its start configuration and rule outputs halt or match a rule input.Source: §3.5 · p. 8

4. Experiments and Results

The pipeline searched active Busy Beaver holdouts and formally verified novel and rediscovered accelerations, with the reported discoveries concentrated in BB(6).

4.1. Implementation

  • The pipeline used Gemini 3.1 Pro with Python simulation and Lean 4.28.1, advancing empirically accurate conjectures through informal evaluation to formal proving.The authors manually validated the final Lean statements, machine definitions, start configurations, and closure theorems.Source: §4.1 · pp. 8–9, §4.2 · p. 9, §4.3 · p. 9

4.2. Experiments

  • The search covered 1,094 BB(6), 65 BB(2, 5), and 4 BB(3, 3) holdouts; an initial run found 52 promising machines, 50 in BB(6).Those machines each yielded at least two conjectures passing the 100% empirical-accuracy threshold; the pipeline then reran them with four attempts per pattern.Source: §4.2 · p. 9

4.3. Results

  • 11 machines received novel accelerations with no comparable prior community analysis, while 15 received alternative or higher-level accelerations for previously conjectured behavior.The latter had not previously been formally verified.Source: §4.3 · p. 9
  • The complete transition-rule systems for the reported machines are provided in Appendix A.The authors report that the corresponding Lean proofs are available in their public repository.Source: §4.3 · p. 9

5. Related Work

The related work spans AI systems for mathematical problem solving and discovery, as well as computational approaches to Busy Beaver and other undecidable-machine frontiers.

Related work on AI mathematics

  • Recent AI systems have solved formalized mathematics problems, but were not designed to autonomously generate conjectures or theories; AI Co-Mathematician relies on human intuition, while AlphaEvolve uses a reward signal (Zheng et al., 2026; Novikov et al., 2025).The passage also cites Olympiad and Putnam results (Liu et al., 2026; Shao et al., 2025) and solutions to open questions (Alon et al., 2026; Feng et al., 2026).Source: §5 · p. 9
  • Mathematical-discovery systems divide conjecture generation from proof writing: ConjectureBench produces statements for theorem provers, while LEAP pairs ideation with Lean formalization (Kung et al., 2026).The passage notes that mathematical conjectures require proof for establishment, although experiments can help test and refine them.Source: §5 · p. 10

Related work on computability frontiers

  • Busy Beaver analysis has relied on community heuristics, including the proof of the fifth value; Claude Opus 4.6 was also used to prove non-halting for many FRACTRAN holdouts (The bbchallenge Collaboration, 2026; Wiki).The passage reports that this work resolved the remaining BB f(21) cases and all but the Fenrir-family Cryptids in BB f(22).Source: §5 · p. 10

6. Conclusion

The paper presents a pipeline for discovering and formally verifying Turing-machine accelerations, reporting novel BB(6) results. Its current scope is limited to Collatz-like dynamics, and the broader mathematical significance of Busy Beaver questions is not assured.

6. Conclusion

  • The pipeline combines empirical pattern detection, LLM-guided conjecturing, informal proving, and Lean 4 verification of Collatz-like transition rules.These rules describe transitions between parameterized tape configurations.Source: §6 · p. 10
  • The system discovered and formally verified novel Collatz-like accelerations for 11 BB(6) machines, provisionally classifying them as Cryptids subject to community acceptance.The authors describe the results as a step toward systematically classifying remaining Busy Beaver holdouts.Source: §6 · p. 10
  • The current approach handles machines exhibiting Collatz-like functions; extending it to other unsolved problems and novel classes of open problems remains future work.The authors note that these structures are already studied by mathematicians and can be exceptionally difficult to resolve.Source: §6 · p. 10

A. Accelerations Discovered by Our Pipeline

  • Appendix A presents the discovered and formally verified transition systems for 11 previously unanalyzed BB(6) machines, with corresponding Lean proofs available in the public repository.Source: A. Accelerations Discovered by Our… · p. 13

A.1. New Discovery: 1RB1LD_1RC0RA_1LA1RE_0LA0LB_0RB1RF_---1RD

For a BB(6) holdout with no previously documented acceleration, the pipeline discovered and formally verified a Collatz-like transition system starting from the blank-tape configuration.

A.1. New Discovery: 1RB1LD_1RC0RA_1LA1RE_0LA0LB_0RB1RF_---1RD

  • The pipeline discovered and formally verified this acceleration for a holdout with no previously documented acceleration.The holdout is the machine named in the section title.Source: §A.1 · p. 13
  • The acceleration represents configurations as A(a,b,c,d) on a tape with parameterized runs of 1s and infinite-zero ends.The displayed starting state is A(0,0,0,0).Source: §A.1 · p. 13
  • Conditional transitions update the parameters and include a halt case at A(0,b,0,b+2).The listed rule applies for any b.Source: §A.1 · p. 13

A.2. New Discovery: 1RB1RD_0LC1RA_0RA1LC_1RA1LE_1RF0LD_---0RE

For a BB(6) holdout with no previously documented acceleration, the pipeline discovered and formally verified an initial P1/P2 system that can be composed into D-state transitions.

A.2. New Discovery: 1RB1RD_0LC1RA_0RA1LC_1RA1LE_1RF0LD_---0RE

  • The machine’s acceleration was discovered and formally verified, first using P1 and P2 configurations and then composing their transitions into D configurations.The initial configurations and the composed D representation are given in the supplied rules.Source: §A.2 · p. 13
  • P1 and P2 transitions route parameterized states into D states, with updates determined by their counter values.The rules include P1(w+2) to D(0,1,w) and P2(a,w+2) to D(a+1,1,w).Source: §A.2 · p. 13
  • The initial staged system starts at P1(1) after 3 raw TM steps, while the simplified D system starts at D(0,1,1) after 13.These are the stated entry points for the two descriptions.Source: §A.2 · pp. 13–14
  • The simplified D configuration is defined with b >= 1, and b odd when a >= 1.This is the stated domain condition for D(a,b,w).Source: §A.2 · p. 14
  • The D transition rules include a halt case at D(0,2k+2,0) and conditional updates for other parameter ranges.The full simplified rule set contains additional cases.Source: §A.2 · pp. 13–14

A.3. New Discovery: 1RB1RB_1LC0RE_---1LD_0RA1LB_1RA1LF_0LE1LE

The paper presents formally verified Collatz-like accelerations for two BB(6) holdouts whose accelerations had not previously been documented by the community.

A.3. New Discovery: 1RB1RB_1LC0RE_---1LD_0RA1LB_1RA1LF_0LE1LE

  • The A.3 acceleration was discovered and formally verified for a holdout with no previously documented acceleration.The machine is identified in the subsection title.Source: §A.3 · p. 14
  • For the A.3 machine, conditional C-state rules transform even-valued parameters and halt from C(2,4,f) or C(2,2,f) when f >= 1.The C configuration is defined for even a and c, with a >= 2, c >= 2, and f >= 1.Source: §A.3 · p. 14
  • The displayed A.3 run begins at C(6,2,2), reached after 76 raw TM steps.This is the stated starting configuration for the acceleration.Source: §A.3 · p. 14

A.4. New Discovery: 1RB0LF_1LC1RA_0RE0RD_---1LE_1LF1RC_1LC1LA

  • The A.4 holdout’s C(a,b) rules use conditional updates and include a halt transition from C(a,2).The displayed starting configuration is C(0,3), reached after 7 raw TM steps.Source: §A.4 · p. 14

A.5. New Discovery: 1RB1RD_0LC1RA_1RA1LC_0RB1LE_1RF0LD_---0RE

Across seven BB(6) holdouts with no previously documented community acceleration, the pipeline discovered and formally verified Collatz-like transition systems.

A.5. New Discovery: 1RB1RD_0LC1RA_1RA1LC_0RB1LE_1RF0LD_---0RE

  • For 1RB1RD_0LC1RA_1RA1LC_0RB1LE_1RF0LD_---0RE, the acceleration reduces intermediate P_1 and P_2 transitions to rules over D_1 configurations.The rules include a halt case for D_1(0, 2k+2, 0).Source: §A.5 · pp. 14–15

A.6. New Discovery: 1RB0LF_1RC1RA_0RD0RB_1LE---_0LA1LE_1RD1LA

  • For 1RB0LF_1RC1RA_0RD0RB_1LE---_0LA1LE_1RD1LA, the pipeline discovered and formally verified a Collatz-like acceleration whose J(0,v,0) and J(0,v,1) rules branch according to v’s parity.J(0,v,0) maps to J(0,0,2v+12) if v is even and J(2,4,2v+7) if v is odd; J(0,v,1) maps to J(2,4,2v+9) if v is even and J(0,0,2v+14) if v is odd.Source: §A.6 · pp. 15–16

A.7. New Discovery: 1RB0LC_0LC1RF_1LE1RD_0RC1RC_0LA1LA_---1RA

  • For 1RB0LC_0LC1RF_1LE1RD_0RC1RC_0LA1LA_---1RA, the acceleration expresses E-configurations through transitions that include parity-dependent cases.The initial system includes auxiliary M_1 and M_0 configurations, which are composed into rules over E.Source: §A.7 · pp. 16–17

A.8. New Discovery: 1RB1LF_0RC1RD_1LA1LD_1LE0RA_---1LC_0LA1LA

  • For 1RB1LF_0RC1RD_1LA1LD_1LE0RA_---1LC_0LA1LA, the simplified C-system specifies parameter ranges that lead to transitions or halting.The rule halts when k = a+4 or k = a+5 in C(a+1, 2k+6).Source: §A.8 · p. 17

A.9. New Discovery: 1RB1RC_1LC1LC_1RE0LD_1LB1RF_---1RA_0RD1RD

  • For 1RB1RC_1LC1LC_1RE0LD_1LB1RF_---1RA_0RD1RD, the merged C-system includes a halt rule when the last two parameters are zero.The system combines two configuration families using C_0(a,b,c) = C(2a,b,c) and C_1(a,b,c) = C(2a+1,b,c).Source: §A.9 · p. 18

A.10. New Discovery: 1RB1LE_1RC1RA_0LD1RB_1LE1LD_1RF0LA_---0RE

  • For 1RB1LE_1RC1RA_0LD1RB_1LE1LD_1RF0LA_---0RE, composing through D yields E-rules with a halt case at E(a, 0, 3).The simplified rules also include transitions conditioned on c being 1 or 2.Source: §A.10 · pp. 18–19

A.11. New Discovery: 1RB1LA_1LC0RE_1LF1LD_1RE0LC_1LB1RA_---0LA

  • For 1RB1LA_1LC0RE_1LF1LD_1RE0LC_1LB1RA_---0LA, composing through M and L yields C-rules including a two-step parameter reduction.The rule C(a+2,b,c,d) -> C(a,b+3,c,d) appears in the simplified system.Source: §A.11 · p. 19

B. Rediscoveries

The Rediscoveries section compares Lean-verified macro-rule systems with previously published community rules for 15 machines.

B. Rediscoveries

C. Candidate Machines

The candidate list records machines whose behavior generated multiple conjectures during the pipeline’s initial conjecturing phase.

C. Candidate Machines

D. Tape Compression Algorithm

The appendix describes an exact tape-compression procedure and gives a Stage 2 prompt that requires candidate proofs to pass strict Lean verification and auditing.

D. Tape Compression Algorithm

  • The compression algorithm represents repeated tape-symbol blocks by a block and repetition count while preserving the head marker and infinite blank regions.Expanding the blocks recovers the original configuration.Source: D. Tape Compression Algorithm · p. 21
  • Block selection favors repeated blocks with a high simplicity score, defined as n|b|, with ties favoring shorter blocks.Candidate block lengths are bounded by the search parameter K, whose default is 16.Source: D. Tape Compression Algorithm · p. 22
  • Boundary adjustment compares coverage from taking n copies versus n−1 and uses one fewer copy only when it strictly increases total coverage.The next block guides this decision but is not yet added to the output.Source: D. Tape Compression Algorithm · pp. 22–23

E. Prompt for Stage 2

  • The Stage 2 prompt requires kernel-compiling proofs with non-vacuous hypotheses, reachable configurations, exhaustive parameter coverage, and rules proved from machine transitions.It also requires zero unproved axioms and audits the exported proof with an independent checker.Source: E. Prompt for Stage 2 · p. 24

Related papers

Loading 2610.22603v2…