Google DeepMind has developed a Gemini-based AI agent capable of autonomous open-ended mathematical discoveries, focusing on the Busy Beaver problem (BB(6)). The agent identified and formally verified acceleration rules for 11 unresolved Turing machines, proposing compact descriptions summarizing execution steps, though whether these machines halt remains unresolved. Each proposed rule underwent informal reasoning and Lean formal proof verification, ensuring results are trustworthy and independent of the model's internal reasoning. This approach demonstrates AI's potential to produce new, formally validated mathematical results. #### 内容简介 推文介绍了来自 Google DeepMind 的一篇论文：一个基于 Gemini 的智能体在开放式数学发现任务中，找到了并用形式化证明验证了对 Busy Beaver 问题 BB(6) 中十一台未解图灵机的新的“加速规则”。由于 Busy Beaver 属于不可计算问题，无法列出固定问题集，智能体需要自主挑选机器、从执行跟踪中发现模式、提出能概括大量步骤的紧凑规则；每个规则先经过非正式推理再由 Lean 形式化证明，只有被证明的规则才被保留。作者将这些未决机器称为“Cryptids”：它们从空带的运行现在有了精确紧凑的描述，但是否停机仍未解决。这是智能体自主选择问题并产出经形式校验的新数学结果的示例。 #### 社区观点 多数评论的共识是“形式化验证（Lean 证明）是关键”，这是让人相信智能体发现结果可靠的主要原因；很多人指出数学是首个出现“AI 找到新东西且可检验”的领域，因为数学结论能被机器或证明检查器严格验证。有人关注模型与流水线细节：论文主流程在 Gemini 3.1 Pro 上运行，但表中显示有 7/11 个新 Cryptids 来自第二阶段使用 Gemini 3.8 Flash 的自动研究智能体；这让人讨论到底是模型能力还是系统化流程起了更大作用。部分评论提出疑问：紧凑描述是否能让人类更容易解决停机问题，还是仍然是另一道难关；也有人强调论文里“可重发现（rediscoveries）”的细节——某些结果曾在社区讨论中出现过，但现在有了 Lean 证明，可信度显著提升。还有观点认为这类工作展示了自动化研究的潜力，但同时提醒不要忽视对方法可复现性、模型选择和证明过程透明性的审视；还有中文评论补充解释了 Busy Beaver 的不可计算性背景与有限候选机的关系，说明 AI 虽然不能解决一般停机问题，但能自主挑选并证明特定机的行为。 #### 内容导读 理解这篇内容可以从三个核心点入手：第一，任务与难度——Busy Beaver（尤其 BB(6)）处在计算理论的前沿且不可计算，研究目标不是穷尽所有情况，而是挑选有趣的机器并试图用紧凑规则描述其长步运行过程。第二，智能体流水线——系统由模型生成候选规则（从执行 trace 中发现模式）、进行非正式推理检验，随后把通过的候选交给 Lean 进行形式化证明；只有经证明的规则才算结果，这一设计把对模型“信任”的问题降到了最低。第三，意义与限制——核心价值在于展示了“智能体能自主选择研究对象并产出经机器核验的数学新知”，这对于自动化科研与可验证发现很重要；但要注意两点：一是这些紧凑规则不必然解决停机问题本身（停机性仍可能未定），二是结果的广泛性依赖于模型版本、自动化策略与证明工具的协同表现。阅读这项工作时，应关注智能体如何生成与筛选候选、Lean 证明的具体形式、哪些结果是全新发现还是社区已讨论过的重证，以及未来将如何扩展到更大或不同类型的数学问题。