AREX Feed Article
Google DeepMind Discovery 团队宣布：Gemini 驱动流水线在 BB(6) 发现 20 个潜在 Cryptids，Lean 4 证明全部开源
2026 年 10 月 21 日 15:00（UTC，北京时间 23 时），Google DeepMind Discovery 团队联合负责人 Tom Zahavy 在 X 上发布：过去一年，由学生研究员 Marco dos Santos 主导的项目用 Gemini 驱动的 agentic（智能体式）流水线研究第六忙海狸数问题 BB(6)，发现了 20 个新的潜在 Cryptids——这类微小图灵机的停机行为等价于尚未解决的数论问题——并为 33 台社区此前研究过的机器补上了验证；全部 Lean 4 形式化证明已开源至 BB 社区的 Discord 频道与 GitHub 仓库。所链论文 《At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier》于 10 月 15 日提交、10 月 19 日修订。
以上数字均为发帖方口径。论文 v2 正文报告的结果更小：11 台此前没有公开分析记录的 BB(6) holdout（停机状态未知的悬留）机器被暂定为新 Cryptids，另有 15 台社区已研究过的机器获得形式化证明；推文与论文对驱动模型的称呼也不一致。论文明确写道，新机器的 Cryptid 归类「有待社区接受」，结论最终以论文与社区验证为准。
图：论文中的流水线示意图（来源：arXiv:2610.22603）
宣发帖原文：从解定理到发现隐藏问题
Zahavy 的 X 自述为 Google DeepMind 的 Discovery 团队联合负责人（Discovery team co-lead）。截至 10 月 22 日，这条帖子显示 31,331 次浏览、371 个赞。
帖子里，Zahavy 把这项工作与常见 AI 数学系统区分开：「大多数 AI 数学系统解决的是人类提出的问题，比如定理；这项工作面对的是数学创造力的另一面：发现隐藏的问题。」按他的说法，BB 社区多年来在寻找「停机前运行时间最长的最简程序」，由于判定这类程序是否停机是不可计算的，没有通用算法可用，进展只能依赖新发明数学技术；社区历史上已在 BB(6) 中认定约 20 台 Cryptids，其中最好的问题被选入社区的 Busy Math Olympiad（BMO）。
推文给出的核心数字是：「借助这条流水线，Marco 和团队发现了 20 个新的潜在 Cryptids，并验证了另外 33 台 BB 社区此前研究过的机器」；「所有证明均已开源，并分享至社区 Discord 频道，我们希望它们能帮助社区朝解决 BB(6) 的方向前进」；团队还「直接向社区 GitHub 仓库提交了相关的停机/不停机证明」。Zahavy 写道，找到这些 Cryptids「揭示了简单程序与数论之间的隐藏联系，帮助数学家绘制计算的边界」，并表示对 Gemini 4 Argon 加速科学发现的能力感到兴奋。
署名方面，论文作者为 Marco Dos Santos、Vivek Veeriah、Alex Havrilla、Andrew Bolt、Goran Zuzic、Satinder Singh 与 Tom Zahavy，署名机构为 Google DeepMind 与剑桥大学；Zahavy 在帖子中说明项目由学生研究员 dos Santos 主导，Hussain Masoom、Maxence Faldor、Moritz Firsching 与 Petar Sirkovic 亦有贡献。
流水线四阶段：从 5×10⁶ 步模拟到 Lean 4 定理
论文（）把系统描述为一条 Gemini 驱动的 agentic 流水线，自动发现图灵机的「加速」（acceleration）——用紧凑的数学规则概括大量执行步骤。实现部分写明：所有 agentic 组件均使用 Gemini 3.1 Pro，配合自研 Python 模拟工具与 Lean 4 交互式定理证明器。四个阶段依次是：
- 模式检测：每台机器先被模拟 5×10⁶ 步，纸带写成「符号块＋指数」的压缩表示，抽取出现频率最高的 100 个抽象模式；
- 猜想：模型把模式归纳成迁移规则并合成代码，再通过合成实验试探边界情形（单次合成迁移的模拟上限 128,000 步），每条规则最多 5 轮修正；
- 非形式证明：生成器—评估器循环（一个 prover（证明者）配两个 critic（批评者）角色，每条规则最多 4 轮），规则必须对所有经验与合成迁移数据达到 100% 预测准确率才能进入下一阶段；
- 形式证明：一个自主智能体直接操作 Lean 4.28.1，直到 Critic 确认所有定理编译通过、没有遗留的 sorry 或未经许可的公理；若撞上 72 小时上限则终止失败。
论文还提到第二阶段：主流水线完成后，团队用接入 Gemini 3.8 Flash 的通用 auto-research（自动研究）系统处理剩余嫌疑机器，让它自行选择目标、为剩余嫌疑机器猜想并证明等价规则，更压缩的加速获得更高计分。
论文的部署与结果：1,094 台 holdouts 里筛出 52 台
按论文的部署方式，系统被投向当前未分类的「活跃前沿」：mxdys 整理的 1,094 台 BB(6) holdouts、BB(2,5) 剩余 65 台、BB(3,3) 剩余 4 台。初始广域搜索找到 52 台有希望的机器（50 台属于 BB(6)），每台至少有 2 条猜想通过 100% 经验准确率门槛；随后团队把这 52 台隔离出来，用更高分辨率设置重跑猜想阶段。
经端到端验证的最终结果分两类：一是 11 台此前没有社区分析记录的机器，系统发现并证明了其空纸带执行恰好由一个 Collatz 型系统（即 3x+1 问题一类的迭代规则）描述——机器停机当且仅当该系统到达停机构型，论文在社区接受的前提下将其暂定为 Cryptids；二是 15 台社区此前在 Discord 等渠道留下过猜想规则、但从未被形式化验证的机器，团队给出了更高层级或替代性的加速及其证明。所有最终 Lean 陈述（机器定义、初始构型、闭包定理）经过人工核对，证明存于团队的公开 GitHub 仓库。
论文的 Table 2（数据截至 2026 年 8 月）给出 BB(6) 的全景：原始机器空间 2.32×10¹⁷ 台，经规范化与判定器压缩后剩 1,094 台 holdouts；社区此前已认定的 Cryptids 计为 18 台——与 Zahavy 帖中「约 20 台」的说法基本一致。若这 11 台新机器全部获得社区认定，BB(6) 的已认定 Cryptids 将增至 29 台。
Cryptid：停机问题伪装成的数论题
Busy Beaver 问题由 Tibor Radó 于 1962 年提出：求 n 状态、m 符号的图灵机从空纸带出发停机前的最长运行步数，记作 BB(n,m)。由于停机问题不可判定，BB(n) 不可计算；要确定 BB(n)=B，必须找到一台恰好 B 步停机的机器，并证明其余机器要么在 B 步内停机、要么永不停机。社区目前已把 BB(2)=6、BB(3)=21、BB(4)=107 和 BB(5)=47,176,870 全部钉死——论文特别指出，BB(5) 的证明「完全没有使用人工智能」，由 bbchallenge 社区协作完成。
卡住 BB(6) 的，正是行为等价于开放数论问题的机器。 的定义是：Cryptid 指空纸带行为可以被一条相对简单的数学规则完全描述、但该规则落在一类未解数学问题里的图灵机；只要存在一台 n 状态 m 符号的 Cryptid，BB(n,m) 就不可能在不解出该数学问题的情况下被解决。这个名字由 Shawn Ligocki 在 2023 年 10 月宣布 Bigfoot 机器的博文中提出；论文举出的具体例子是 Antihydra——2024 年 6 月由 mxdys 发现、racheline 证明其 Cryptid 身份的一台六状态、两符号机器。wiki 还收录了一台 BB(25) 机器：当且仅当哥德巴赫猜想为假时它才停机，其行为已在 Lean 中验证。
论文解释了这类规则的形状：纸带被表示成符号块序列，块长即指数，机器的演化成为按奇偶等模条件切换更新的分段仿射映射。论文同时引用 Conway 1972 年的结果提醒：对一类广义 Collatz 映射，判定轨迹是否到达目标本身就是不可判定的。对这 11 台新机器而言，流水线得到的是精确的数学描述而非停机答案。
推文与论文对不上的三处口径
把推文与论文 v2 对照，至少有三处差异。
数量：推文称「20 个新的潜在 Cryptids、验证 33 台机器」，论文正文与 Table 2 报告的是 11 台新机器、15 次重发现、52 台候选。两组数字无法相互对应，帖子也没有给出换算口径。
模型：推文两处称流水线由 Gemini 4 Argon 驱动；论文实现部分写明所有 agentic 组件使用 Gemini 3.1 Pro、第二阶段另用 Gemini 3.8 Flash，全文没有出现 Argon 或 Gemini 4 字样。
认定状态：论文自述其采用的 Cryptid 定义「比 Busy Beaver 社区的惯常含义更宽」，因此对新机器的归类「仍取决于社区接受」；推文虽用「potential Cryptids」一词，但整体表述更接近既成结论。
开源渠道方面，推文称全部证明分享至社区 Discord 频道并直接提交了社区 GitHub 仓库。不过，显示，其中最近一次推送是 2026 年 9 月 29 日的 bbchallenge 前端仓库，目前看不到与这批证明对应的提交；相关内容也可能以拉取请求或团队自有仓库的形式发布，以社区渠道的公开记录为准。
论文写明，判定这些机器的轨迹是否到达停机构型仍是未解问题，也是完成相应 Busy Beaver 分类的中心障碍。这 11 台机器最终能否被社区正式收录为 Cryptids、推文与论文的数字差异作何解释，答案都还在 bbchallenge 社区手里；BB(6) 其余的 holdouts 也仍在等待各自的结局。