Agent 做出的证明，为什么还需要第二个机器来相信

一个 Agent 花了 11 天，写出 1,300 万行 Lean 代码，最后得到一份被计算机检查过的费马大定理证明。这个故事很容易被讲成“模型已经会做数学了”。但对产品团队而言，更值得拆开的不是模型有多聪明，而是一个更硬的问题：当 Agent 的输出可能很长、很复杂、很难由人逐行复核时，什么东西才算可以交付的结果？

Anthropic 在 Formalizing Fermat's Last Theorem 中给出的答案，是把“探索”和“相信”拆开。Claude 负责提出定义、补全中间定理、并行尝试证明路径；Lean 负责检查逻辑；Prove2Me 负责维护定理依赖图、编译与搜索；人类只给出少量高层方向，并审阅最终产物。

这不是把模型换成一个更大的模型就能复制的结果。它更像一个发布契约：模型可以自由探索，但最终状态必须由独立、可重放、可拒绝的验证器锁定。

文中关于费马大定理形式化过程、时间、代码量、定理数和 token 消耗的数字，均来自 Anthropic 的官方文章。关于产品架构、验收门槛和指标的部分，是基于这些事实的产品化解读，不代表 Anthropic 已公开承诺的通用方案。

先看交付物，而不是先看模型#

Anthropic 报告的对象不是一段自然语言答案，而是一份可以交给 Lean 的形式化证明。Claude 在 11 天里完成了端到端的费马大定理形式化，沿途生成了约 1,300 万行 Lean，证明了 30,300 个定理，其中 29,500 个被最终证明使用。文章称这是第一份完整、由计算机检查的费马大定理证明。

这个结果有三个层次，不能压成一句“Agent 证明了定理”：

层次	原文事实	对产品的含义
探索	数十个 Claude Agent 协作定义概念、证明中间定理，再逐步攻克更难的命题	生成过程可以并行、发散，允许失败样本存在
结构	Prove2Me 用有向无环图维护定理状态，并把定理陈述与证明文件分离	长任务需要可查询的状态图，而不是把上下文全塞进对话
验证	Lean 检查最终证明；比较器确认定理陈述与 Mathlib 中的版本一致	交付物必须能被独立程序拒绝，而不是只由生成者自评

产品验收也应该按这三层拆开。模型输出“看起来合理”只能通过探索层；只有依赖完整、编译通过、对象身份匹配，才算验证层通过。

失败不是异常，而是状态图的一部分#

Claude 的早期尝试很快失去项目状态，Agent 之间也停止了有效协作。文章称，这些失败努力最后贡献了约 7% 的非样板代码。成功的转折不是换一个更长的提示词，而是引入 Prove2Me：

1. 用定理依赖 DAG 告诉 Agent 下一步该尝试什么，减少记忆退化；
2. 把定理陈述和证明拆到不同文件，单独维护链接，加快 Lean 编译并减少资源消耗；
3. 为每个定理保存自然语言描述，方便搜索和复用已有结果。

这组设计对普通 Agent 产品同样适用。长任务的最小状态单元不应该是“上一轮对话”，而应该是可定位、可依赖、可重试的对象。例如：一个数据库迁移提案、一条代码变更、一份合同条款或一个实验结论，都应该有稳定 ID、父依赖、当前验证状态和失败原因。

如果失败只存在于上下文里，下一次运行只能重新猜；如果失败写回状态图，它就能成为下一条路径的约束。失败样本不是日志附件，而是搜索空间的一部分。

生成者不能给自己当裁判#

这次工作里最关键的分工，是 Claude 并不拥有最终真值。它可以写 Lean、修错误、推进定理，但“证明是否成立”由 Lean 的检查器判断；定理是否就是要证明的那个对象，则由比较器与 Mathlib 的陈述比对。

这比“让另一个 Agent review”更严格。另一个 Agent 仍然可能共享同一套误解、同一份上下文和同一种失败模式。独立验证器至少要满足四个条件：

• 输入边界明确：只接受声明、证明文件和允许的依赖，不接受生成者口头解释作为证据；
• 失败可见：编译错误、未满足的依赖和对象不匹配都要返回机器可读的原因；
• 重复运行稳定：同一份输入在同一版本验证器上应得到相同状态；
• 权限更小：验证器不替生成者修改结果，也不替业务系统执行副作用。

在 AI 产品里，这个“第二个机器”可以是类型检查器、策略引擎、沙箱测试、数据库约束或审批服务。模型负责提出候选动作，系统负责决定候选动作是否能进入下一状态。

把“可验证”写成发布门槛#

Anthropic 的文章说，Claude 的证明最终只使用 Lean 的三个标准公理；一个比较器确认定理陈述与 Mathlib 的陈述一致。它还说明，整次工作消耗了约 60 亿输出 token，使用的是一个大致可比 Claude Fable 5.1 的内部通用研究模型。这些信息同时告诉我们两件事：结果很强，但成本也是真实约束。

我会把长程 Agent 的发布门槛写成一张不允许互相抵消的契约：

门槛	最小证据	不通过时的处理
对象一致	输入目标、版本和最终对象有稳定 ID；比较器确认没有“证明了另一个问题”	阻止合并，要求重新绑定目标
依赖完整	所有父定理、工具版本和数据快照可定位	标记为不可重放，不进入生产
独立验证	检查器在干净环境中通过，且没有生成者写权限	降级为候选结果
失败可回放	失败输入、错误和最后状态可以再次运行	进入人工复核或缩小任务范围
资源可控	token、编译时间、并行度和重试次数在预算内	停止扩张，保存当前状态

这张表的重点是“不可抵消”。验证通过不能掩盖成本爆炸；成本低也不能替代对象一致性。产品上线时应分别设硬门槛，而不是做一个总分。

60 亿 token 不是模型价格表#

60 亿输出 token 是一次研究工作的消耗，不是任何产品都会遇到的单次成本。它包括数十个 Agent 的探索、失败和重复尝试，不能直接拿来估算一次用户请求的价格。但它足以提醒产品经理：长程 Agent 的成本单位不应只是“每次 API 调用”，而应是“完成一个可验证任务需要多少探索”。

我会追踪四个任务级指标：

1. 每个可验证任务的总 token：包括失败尝试、修复和验证，不把失败成本藏在平均调用价里；
2. 从首个候选到通过验证的墙钟时间：并行度提升可能降低时间，却增加编译和协调成本；
3. 验证通过率与重放通过率：第一次通过不代表换一台机器、换一个干净环境仍能通过；
4. 状态复用率：已有定理、测试夹具、工具结果被下一次任务复用多少，而不是重新生成多少。

如果产品只报“模型回答成功率”，它会把大量不可交付的中间产物算成成功。对于研究、代码、金融或合规任务，真正的分母应该是完成并通过验证的任务数。

人类仍然需要看懂结果#

Anthropic 明确写道：形式化证明不应取代面向人的解释。Lean 可以证明逻辑链条符合公理，但它不会自动告诉产品使用者为什么这条链条值得相信、假设是否适合业务，或结果是否回答了真正的问题。

所以我不会把“机器可验证”当成唯一交付物，而会要求双层产物：

• 机器层：声明、依赖图、证明/测试、验证器版本、编译日志和可重放命令；
• 人类层：目标是什么、用了哪些假设、哪些部分由 Agent 探索、哪些部分由人确认、失败过哪些路径、结果不能推断什么。

机器层防止逻辑错误，人类层防止目标错配。缺少前者，系统无法稳定验收；缺少后者，团队可能在“证明正确”的对象上做错产品决策。

面向产品经理的最小实现#

如果要把这套思路落到一个能调用工具的 Agent，我会先做一个很小的闭环：

1. 把用户目标编译成带版本的任务声明，而不是直接放进长对话；
2. 让 Agent 产生候选计划和中间对象，每个对象写入状态图；
3. 用独立验证器检查格式、依赖、权限和业务约束；
4. 只有验证通过的对象才能触发下一步工具调用或人工审批；
5. 保存失败样本和验证日志，下一次运行优先复用已验证的节点；
6. 在灰度期间同时看任务成本、重放成功率、人工推翻率和副作用事件。

这比一开始就做“多 Agent 自主研究平台”更容易验收。先证明一个对象能从声明走到验证通过，再扩大并行度、工具数量和任务范围。

这次结果能证明什么，不能证明什么#

原文能支持的判断是：在 Anthropic 描述的设置里，Claude 与 Prove2Me、Lean 和 Claude Code 多 Agent harness 协作，在 11 天内完成了一个大规模、端到端、计算机检查的费马大定理形式化项目；状态图、定理复用和独立检查是成功链路的一部分。

原文不能证明：Claude 已经独立发现了新的数学定理；任何长任务都能在 11 天内完成；60 亿 token 是可复制的标准成本；多 Agent 在所有任务上都优于单 Agent；或者一份机器检查通过的证明天然就是对业务有用的答案。文章还说明证明遵循了 Darmon、Diamond 和 Taylor 对 Wiles 证明的简化版本，并依赖既有的 Lean、Mathlib 与社区形式化工作。

因此，产品团队不应把这次成果包装成“模型取代数学家”。更可靠的解读是：当生成空间越来越大，验证器、状态图和可重放产物会成为能力本身的一部分。

来源与边界#

• 原始来源：Anthropic，Formalizing Fermat's Last Theorem，发布于 2026 年 9 月 4 日，分类为 Science。文章由 Anthropic 发布，文中明确介绍了研究员 Tianyi Peng 及其 Columbia University 形式化工具团队的工作。
• 研究对象：Claude 参与的费马大定理（FLT）Lean 形式化项目；证明遵循 Darmon、Diamond 和 Taylor 对 Wiles 证明的简化版本，不是重新发现一份与既有数学无关的新证明。
• 系统设置：Claude Agent 负责定义概念、证明中间定理和协作推进；Prove2Me 维护定理 DAG、分离声明与证明文件并提供搜索；Lean 检查逻辑；比较器核对定理陈述与 Mathlib；人类只提供少量高层方向并审阅产物。
• 关键数字：11 天；约 1,300 万行 Lean；沿途 30,300 个定理、最终使用 29,500 个；约 60 亿输出 token；数十个 Agent 协作；早期失败努力贡献约 7% 的非样板代码。Anthropic 还报告了三个 Claude Max 计划协作三天形式化 Vinogradov 三素数定理的实验。
• 结果边界：这些数字和“第一份完整、计算机检查的证明”是 Anthropic 官方报告；本文没有独立复现实验，也没有把它当作受控的模型能力 benchmark。文章没有提供单 Agent、不同模型或不同 token 预算下的同协议对照，因此不能推出多 Agent 的普遍优势、固定成本或通用完成时间。
• 本文产品化解读：把生成者与验证器分离、把失败写回状态图、用任务级成本和重放通过率做门槛，是基于上述事实的产品设计推演，不是 Anthropic 已公开的商业产品承诺。