千个智能体自己分工重证费马大定理：28.7小时、输出词元仅为原版三分之一
核心概要
Anthropic 让 1000 个运行 Claude Fable 5.2 早期版本的智能体，在没有 Prove2Me 平台、也没有研究员指挥的条件下，仅凭 Git 和共享 SQL 数据库重做了费马大定理的形式化证明。团队用 28.7 小时完成，输出词元约为此前由研究员加数十个智能体、耗时 11 天完成的那次形式化的三分之一，写出的证明长度约为原来的七分之一。这是一次玩具实验，作者称它说明此类智能体团队能在精心设计的安全边界内完成长周期目标。
深度剖析
多智能体团队可以不再依赖专用协作平台和研究员调度，自己组织起来完成一项长周期数学形式化任务。 此前的费马大定理形式化由一名研究员和数十个智能体用 11 天完成，依赖 Prove2Me 平台把待证命题拆成子命题的共享图来协调，并由研究员把握方向。 新实验中 1000 个智能体在 28.7 小时内完成证明，输出词元为原版的三分之一，证明长度为原版的七分之一。
协调靠智能体自己在共享数据库里建表完成，而不是靠预先设计的图结构。 Prove2Me 用共享图记录命题拆分和进度，每个命题单独成文件以便并行编译。 运行开始 10 分钟内，负责的智能体在 Postgres 中建了五张表，分别用于发布指令、分配任务、公开笔记、子任务认领和完成记录，随后向分配表写入 999 行，把 60 个命题分给 16 至 17 人一组的小队。
最难的部分由团队自发生成任务树拆解，最终在 28.4 小时被证明。 Langlands–Tunnell 的队长此前估计至少需要 70 万到 100 万行 Lean 代码，按时完成概率不足 1%，负责智能体一度把它搁置。 约 750 个助手被调往该命题后，任务树扩展到 2418 个任务、最深 10 层，该命题在第 28.4 小时完成，最终定理在第 28.7 小时完成。
启示与展望
这是一次玩具实验，任务范围限于 60 个给定命题的 Lean 形式化，智能体在无网络访问的沙箱中运行，只通过 Git 和共享数据库协作。作者明确表示该结果并不取代领域专用工具或平台，Prove2Me 这类平台仍可能通过加快 Lean 编译、检索复用人类结果来提高效率。
作者称这是玩具实验，并指出智能体倾向于放弃难题、误判难度：早期助手判定 60 个命题中有 47 个在预算内不可行，团队后来仍证明了其中大多数。作者还表示，本次运行只用了基于动作的监控，思维链监控是在运行之后才加入的。