TWITTER / X
Google DeepMind 论文：Gemini 智能体在 Busy Beaver 问题前沿自主发现并经 Lean 形式化验证的加速规则
网友 elvis 推荐的 Google DeepMind 论文（arXiv:2610.22603）介绍了一种基于 Gemini 的智能体，在 Busy Beaver 问题当前前沿 BB(6) 上自主发现并对十一条未解决图灵机的加速规则完成了形式化验证。Busy Beaver 问题不可计算、没有固定问题清单，智能体需自行挑选机器、在执行轨迹中发现模式并提出可压缩多步的紧凑规则；每条规则先经非形式推理，再由 Lean 证明，仅保留已证明的规则，因此结果不依赖对模型推理的信任。作者暂定将这些机器称为 Cryptids：它们从空白磁带出发的运行现在有了精确的紧凑描述，但是否停机仍是开放问题。转发者认为这是智能体在自己选择的问题上产出新的、经形式化检验的数学成果的早期范例。以上为原文陈述，论文具体内容未经独立核实。
AI 解读
这是 AI 辅助科学发现的标志性案例：智能体承担问题选择、模式发现与猜想提出，Lean 形式化证明则提供了不依赖模型可信度的验证闭环。若结论成立，说明 LLM 智能体已能在不可计算问题（无固定数据集）上自主产出新的、可机器检验的数学结果，对 AI for Math / AI for Science 方向有重要示范意义。不过论文为新发布内容，其验证范围与结论强度（如"acceleration rules"的实际效果）需阅读原文确认；作者声称其为代表性早期工作，转发者亦称之为"exciting work"，均属主观评价，不应作为事实采信。
推文原文
RT elvis Banger paper from Google DeepMind on open-ended math discovery with agents. This is one of the early, exciting works I have seen on autonomous AI-powered discoveries. (bookmark it) A Gemini-based agent found and formally verified new acceleration rules for eleven unresolved Turing machines in BB(6), the current frontier of the Busy Beaver problem. Busy Beaver is uncomputable, so no fixed list of problems exists. The agent has to pick machines, spot patterns in their execution traces, and propose compact rules that summarize many steps at once. Each proposed rule then goes through informal reasoning and a Lean proof. Only proved rules are kept, so the result does not depend on trusting the model's reasoning. The authors provisionally call these machines Cryptids. Their runs from a blank tape now have exact, compact descriptions, but whether they halt is still open. This is a good example of an agent producing new, formally checked mathematical results on problems it chose itself. https://arxiv.org/abs/2610.22603 Chat with Paper: https://academy.dair.ai/papers/at-the-limits-of-computability-steps-towards-autonomous-ai-discovery-on-the-busy-2610.22603