11 天，1300 万行 Lean，29,500 个被最终证明实际使用的中间定理。

这个数字很容易被读成又一次模型能力发布会。Anthropic 9 月 4 日公开的成果却比跑分有意思得多，Claude 在一个多 Agent 协作环境里完成了费马大定理的端到端机器检查形式化证明。最后交给 Lean kernel 检查，外加独立的 Rust 实现 nanoda 复核。

我把官方说明和开源仓库走了一遍，最想聊的不是 Claude 会不会做数学。

而是一个更贴近工程的问题。一个 Agent 团队究竟怎样才配得上「完成了任务」这几个字？

很多团队现在做 Agent，终点仍然是一段看起来挺对的自然语言，或者一次 CI 能过的提交。前者太软，后者也没想象中硬。费马大定理这个项目给出的答案很激进，也很实用，Agent 的产物应该尽可能落到一个能独立验收的系统里。模型负责探索、拆解和生成，可信度交给一个比模型小得多、规则更清楚的验证器。

这不是数学圈的孤立新闻。对写 Java 服务、搭 LangGraph 工作流、维护 CI/CD 的人，它更像一张提前送来的架构图。

1300 万行代码，并不等于 1300 万行可信结论

先把事实摆在桌面上。

费马大定理说的是，当指数大于 2 时，不存在正整数 a、b、c 让 a 的 n 次方加 b 的 n 次方等于 c 的 n 次方。1995 年，Andrew Wiles 的证明发表时长达 129 页，背后牵涉椭圆曲线、模形式和 Galois 表示。更麻烦的地方不在于它长，而在于人类论文允许跳步，允许一句「由一个标准引理可得」。

Lean 不吃这一套。

Lean 是 proof assistant。你可以把它理解成一个对逻辑非常较真的编译器。自然语言里的「显然」，在它那里要展开成明确的类型、定义、引理和推导。前面的一个符号没对上，后面的高楼就不会假装站着。

Anthropic 公开的仓库把最终命题写得很直白，n ≥ 3，且 a b c 都为正整数时，a ^ n + b ^ n ≠ c ^ n。仓库里的 FinalCheck.lean 不只是编译这个命题，还会检查它只依赖 Lean 的三个标准公理，随后把它和 Mathlib 中的表述对照。另一个独立 Lean kernel 实现 nanoda 也接受了同一份环境导出。

这层区分很关键。

Claude 生成了海量代码，不等于 Claude 的每一步都值得信任。值得信任的是，最终那条命题能不能被一个确定性的、范围很小的 checker 重放出来。仓库 README 甚至专门提醒，工具能检查形式命题、依赖和公理，无法替你判断每个中间定理的名字是不是名副其实。

坦率的讲，这比很多「模型完成复杂任务」的宣传诚实得多。它没有把信任全部压在模型身上，也没有假装 verification 能解决所有语义问题。能证明的，交给 kernel。人仍然要看问题定义是否对，目标是否对，接口是否对。

这套分工，正是 Agent 工程最缺的东西。

这不是一个会写 Lean 的单体 Agent

如果只看标题，很容易脑补成 Claude 对着一个超长 prompt 连续思考 11 天。真实过程没有这么浪漫。

官方披露的协作方式更像一个有共享任务图的工程团队。数十个 Agent 在 Prove2Me 平台中定义概念、领取子问题、证明中间引理，再把结果挂回依赖图。最终项目产生了约 30,300 个可验证定理，其中 29,500 个进入最后证明。它消耗约 60 亿输出 token，使用的是一款接近 Claude Fable 5.1 的内部通用研究模型。

把数学语言翻译成工程语言，大概是这样。

  • 费马大定理是 root task
  • 每个引理是一个可验收的 task node
  • 前置定理构成 dependency graph
  • Lean 编译结果是 node 的验收门
  • 通过的节点才会成为下游 Agent 可以引用的 artifact

你想想看，这和一个靠谱的后端交付没有多大差别。订单系统要上线，不能让十个 Agent 各写一段「我觉得没问题」的报告。你需要 API contract，需要 migration 检查，需要 integration test，需要可回滚的发布物。复杂性不是靠把 Agent 数量堆上去消失的，它只是换了一种形态，变成状态、依赖和验收边界。

Anthropic 一开始也踩了这个坑。官方文章写得很具体，早期 Agent 虽然做出了一些进展，却很快丢失项目状态，协作失效。失败尝试留下的内容，约占最终证明非样板代码的 7%。后来切到 Prove2Me，事情才开始收敛。

这段失败比成功本身更有参考价值。

很多人把 multi-agent 的难点理解成 prompt 要不要写得更聪明。我一直觉得，真正难的是让后来者看得懂前面的人到底做了什么，哪些已经确认，哪些只是猜测，哪个结果可以复用，哪个结果必须推倒重来。没有一个外化、可检索、可验证的状态层，Agent 再强，也只是在接力赛里反复丢棒。

共享记忆不是聊天记录，而是一张能被执行的任务图

现在常见的 Agent memory 大致分两类。

一类是把对话摘要塞进 context。它解决的是「别忘记用户刚才说过什么」。另一类是向量检索，解决「从历史文本里捞出相关片段」。这两类都重要，但它们不是项目状态。

项目状态至少要回答四件事。

  • 当前目标被拆成了哪些可交付节点
  • 每个节点的输入、输出和验证结果是什么
  • 哪些节点已经冻结，哪些还允许修改
  • 某个失败发生后，影响范围到哪里

Prove2Me 的价值不只是存储内容，而是让定理、依赖和证明状态有了机器可读的身份。一个 Agent 不是把一段文字扔进群里，而是产出一个下游可以引用、验证器可以重放的对象。

回到 LangGraph 这块，很多图工作流已经有 node、edge、checkpoint 和 state。可现实里，state 往往只是一个不断膨胀的 JSON。它记录了做过什么，却很少记录「这个结论为何成立」以及「一旦上游变了，谁必须重新跑」。

我的感受是，下一阶段的 Agent state 不该只是一份 context payload。它更像 build system 的 DAG，加上一份带 provenance 的 artifact registry。

举个很日常的例子。让 Agent 给 Spring Boot 服务做一次依赖升级，任务图可以拆成依赖兼容性检查、编译、单测、关键接口 smoke test、容器镜像扫描、变更说明。每一步不是一句「完成」，而是一个带输入 commit、命令、日志摘要、产物 hash 和 verdict 的节点。上游版本变了，下游节点自动失效。谁接手都不需要先读两万字聊天记录。

这才叫记忆。

验收器要小，不能再找一个大模型当裁判

这里有个很容易犯的错。既然生成者不可靠，那我再放一个 Agent 做 reviewer，不就行了？

不太行。

一个模型检查另一个模型，当然能筛掉很多低级错误。但两边可能共享同一种误解，也可能在长上下文里一起漂移。更糟的是，review 的判断本身很难稳定重放。今天它说通过，明天换个温度参数又说有风险，这很难变成工程流程的地基。

费马项目采用的是更朴素的路线，缩小可信计算基。

Lean kernel 的规则相对小，输入和输出确定。证明是否通过，不取决于 Claude 今天心情如何，也不取决于一段评审 prompt 写得够不够花。仓库还引入独立实现的 nanoda 做交叉检查，这个动作很像安全领域里的 N-version verification。不是再加一个聪明的裁判，而是用不同实现去检查同一个明确规范。

这话听着有点刺耳但，Agent 系统的目标不该是把模型包装成「永远正确」。模型会误解、会偷懒、会在看似合理的地方漏掉边界。

工程上更现实的目标是，把错误尽量赶到一个便宜、确定、能自动失败的位置。

对于软件交付，这个 verifier 可以是类型系统、编译器、契约测试、数据库约束、静态分析、policy-as-code、replayable workflow。对于运维动作，可以是 Terraform plan、OPA policy、变更窗口规则和健康检查。对于数据任务，可以是 schema、质量阈值、血缘校验和可复算的 query。

反正我觉得，一条 Agent pipeline 的成熟度，不该看它能生成多漂亮的最终说明，而该看失败时会不会明确停住，留下可追踪的证据。

人类角色不是被挤出流程，而是往上移动

看到「11 天基本自主完成」，有人会自然担心，人是不是只剩点确认按钮的工作。

我不这么看。

在这次项目里，人没有替 Agent 逐行写 Lean，却仍然做了几个无法省略的判断。选择什么证明路线，判断 Jacobian、Mazur 相关工作哪个优先，决定平台与协作方式，设计最后相信什么验证器。这些不是把一个子任务拆得更细就会自动出现的答案。

Wiles 的故事也提醒我们，验证从来不是打勾动作。1993 年的证明报告后，两个月的审查发现了关键缺口。他和 Richard Taylor 又花了一年修复，才在 1995 年发表正确版本。机器形式化降低的是逻辑链断裂后不被发现的概率，不会替人定义什么问题值得解决，也不会替人判断一条形式化路线在数学上是否有解释力。

不是说人类审阅不重要，而是它的位置该变了。

让人去读每一条 Agent 的过程日志，既慢也不可靠。更好的分工是，人负责目标、约束、风险取舍和验收标准，机器负责大规模搜索、落实细节和重复检查。人类评审者看到的是一张任务图、一组关键假设和一套可重放证据，而不是一个黑箱吐出来的结论。

这和 Channing 做 AI 平台落地时常碰到的情况很像。业务方说「给我一个会自动处理的 Agent」，真正需要追问的是，它能动哪些系统，什么条件下能提交，失败时谁接管，日志能不能复盘。答案从来不在某个更长的 system prompt 里。

别把 11 天当成生产力 KPI

还有一盆冷水得泼。

1300 万行 Lean 不适合被当成「AI 写代码能力」的 KPI。它是为 machine checking 展开的形式化工件，不是 1300 万行人类要维护的业务代码。项目用了约 60 亿输出 token，成本和基础设施要求也远不是普通团队可以照搬的水平。即便 Anthropic 说过三个个人 Claude Max 订阅曾在三天内协作完成 Vinogradov 三素数定理的一部分形式化，这也不等于随便开几个窗口就能重演费马大定理。

更重要的是，形式验证特别适合数学这类有精确定义、明确推理规则的领域。真实业务里的「给用户一个合理退款」「不要误伤正常账户」往往先缺的是规范，不是模型能力。你不能把一句模糊的产品愿望塞进 Lean，然后期待得到一道绝对正确的答案。

说实话我也不确定，多少 Agent 产品会愿意为严格验证付出额外成本。验证器、契约和回放机制都要建设，短期看确实比再调一次 prompt 麻烦。

但当 Agent 从写辅助代码走向改生产配置、执行采购、触发支付、操作浏览器时，这笔账迟早要算。模型越能行动，系统越不能只靠模型自证。

可以从明天开始做的三件小事

不需要等到团队引入 Lean，也不需要把每个业务规则写成定理。可以先做三件没那么酷、却真的管用的事。

第一，把每个 Agent 节点的完成定义改成可验证的 artifact。不要只保存自然语言摘要。保存输入版本、输出文件、执行命令、校验结果和失败原因。这样才知道结果能不能被下游使用。

第二，给高风险动作补一个确定性的 gate。部署前跑测试和 policy，写库前做 schema 与幂等检查，外部调用前做额度与权限校验。模型可以提议，gate 决定能否真的落地。

第三，让任务图支持失效传播。一个上游工具版本、需求约束或数据源变动后，哪些结果还有效，哪些必须重新执行？这块需要注意一下，不然所谓长期记忆只会变成陈旧知识的仓库。

这三件事听起来没有 multi-agent swarm 那么刺激。

可它们决定了 Agent 系统是在演示里显得聪明，还是能在生产环境里让人睡得着。

费马当年那句「这个页边距太窄，写不下我的绝妙证明」，后来困住了数学家三百多年。今天 Claude 把一条漫长的证明塞进了 1300 万行 Lean。它带来的真正提醒不是「模型已经替代数学家」，而是另一件更朴素的事。

当机器开始大量产出结论，能让结论经得起复查的系统，会比产出结论的机器更稀缺。

资料