arXiv cs.AI· Marco Dos Santos, Vivek Veeriah, Alex Havrilla, Andrew Bolt, Goran Zuzic, Satinder Singh, Tom Zahavy·· 12 小时前AI 评分52
面向 Busy Beaver 前沿：基于 Gemini 智能体流水线的自主数学发现
At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier
AI 导读
论文提出一条基于 Gemini 的智能体流水线，在不可计算的 Busy Beaver 领域自动发现图灵机加速规则，把多步执行压缩为紧凑的数学规则。该系统整合模式识别、自动猜想、非形式化数学推理与 Lean 形式化定理证明，自主发现并形式化验证了 BB(6) 中 11 台机器的新型 Collatz 式加速。
正文 · 原文
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.
| Subjects: | Artificial Intelligence (cs.AI); Formal Languages and Automata Theory (cs.FL) |
| Cite as: | arXiv:2610.22603 [cs.AI] |
| (or arXiv:2610.22603v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.22603 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Vivek Veeriah [view email]
[v1]
Thu, 15 Oct 2026 19:56:48 UTC (379 KB)
来源：arXiv cs.AI · arxiv.org