检查器只审证明，
不审题目

这一次，数十个 Claude agent 基本自主地工作了 11 天，写出 1300 万行 Lean。Lean 是一种证明助手：人或 agent 把数学写成代码，Lean 的内核再逐步检查推理。项目共生成 30,300 条定理，其中约 29,500 条进入最终证明；依赖树中的精确数量是 29,511 条。整份证明是 Mathlib 的 5 倍多。Mathlib 是 Lean 社区维护的数学库，也是这份证明的基础。

这些 agent 使用的不是在售模型，而是一款内部研究模型。官方称，它的能力大致相当于 Claude Fable 5.1。项目消耗了约 60 亿输出 token。

伦敦帝国理工学院纯数学教授 Kevin Buzzard 受邀审阅了这项工作。他自 2024 年起领导另一项由 EPSRC 资助的费马大定理形式化项目。Buzzard 认为：AI autoformalization artefacts are now robust enough to be built upon。随后，他独立编译代码库，并运行 comparator，核对最终陈述与 Mathlib 中的费马大定理陈述是否一致。他在自己的 Xena 博客上给出结论：it checks out。

Buzzard 同时写道：mathematically this work of anthropic tells us essentially nothing。他此前已经有 99.9% 的把握相信原有数学证明成立。因此在他看来，这项工作的价值不在于发现了新数学，而在于展示 AI 自动形式化已经能做到什么。

成功之前还有一批失败尝试。Anthropic 博客只用一段话解释原因：agent 起初有一些进展，但很快丢失项目状态，无法继续有效协作。原文是：while agents had some early success, they quickly lost track of the project's state and stopped collaborating effectively。这些尝试并非全被丢弃，最终证明中约 7% 的非模板行来自它们。

转机来自开放协作平台 Prove2Me。它由 Anthropic 研究员、哥伦比亚大学商学院助理教授 Tianyi Peng 及其团队开发。Lean 一直都在，题目也没有变。博客所说的故障发生在 agent 的协作层：它们无法持续共享项目状态。

本文不展开费马大定理的数学细节，只分析这套协作结构。检查器可以保证证明推出某条陈述，却不能保证这条陈述忠实表达了原本要证明的数学命题。几十个 agent 分别写陈述时，检查器也不会判断这些陈述能否彼此兼容。Prove2Me 处理的正是这一层。

同一研究线上的 fanout-needs-a-referee 讨论了另一种做法：由一个 coordinator 单线程指挥约 60 个 subagent，并判断它们的结果。相比之下，这次运行把共享状态从 coordinator 的上下文移到了平台上的公共陈述账本。

Anthropic 博客对失败原因只给了一句：agent 丢失项目状态，无法继续有效协作。博客没有提供更完整的因果分析。它只说换用 Prove2Me 后项目成功了，并列出平台提供的三项帮助。最终证明中约 7% 的非模板行来自此前的失败尝试。

Prove2Me 论文解释的是平台为何采用现在的设计。论文先讨论一种看似直接的协作方式：在一份大证明里留下许多 sorry，让多个 agent 共同编辑文件，各自填补空缺。

这种方式首先会增加计算开销。下游引理一旦改变，依赖它的上游文件可能都要重新编译，而 Mathlib 这样的大型库从头构建本来就很慢。

更根本的问题是任务难以独立拆分。多个 agent 同时修改一组文件，改动会彼此纠缠，很难把一项工作完整地交给某个参与者。Git 和 PR 可以缓解冲突，但每个 PR 都需要人或编排 agent 审核并合并。对去中心化平台来说，这个中心步骤的代价太高。

论文还区分了两类共识失败。第一类是没有共享目标：多个 agent 把同一条引理写成互不兼容的陈述，这些陈述无法相互 import。于是并行工作变成重复工作，结果也无法累积。

第二类是陈述漂移：一条中间陈述悄悄偏离原文，所有 import 它的 proof-sketch 都会继承这个偏差。

内核无法识别这两类问题。它只会逐条检查每个陈述对应的证明。

Anthropic 随博客发布了一份 17 页 PDF，记录每天的进展和 Claude 的推理原文。Day 1 是 2026 年 8 月 7 日。PDF 说，除了目标定理的一行陈述，人没有编写其他数学内容或 Lean 代码。原文是：wrote no mathematics and no Lean beyond the one-line statement of the goal theorem。

运行期间，人偶尔调整优先级或给予鼓励。博客保留了两句指令："Jacobian as a scheme sounds high priority," "push [the] Mazur [theorem] to be done soon."

因此，人的角色不能简单概括成“只写了一行题目”。在这次运行中，人写下目标定理，并偶尔调整优先级。按照 Prove2Me 论文描述的 mission 设计，人还要审核目标陈述、定义和 milestone。不过，博客和 PDF 没有说明这次 mission 的 milestone 由谁制定或审核。

PDF 对 agent 分工的描述很直接：数十个 Claude agent 并行编写陈述、互相检查，再完成证明。原文是：A team of Claude agents working in parallel wrote the statements, checked one another's statements, and proved them.

通常，一条陈述在进入证明阶段前还会经过同伴检查。PDF 说：Before a statement was worked on, other agents usually checked that it was true as written. This caught several false statements early.

时间线记录了多次互查。Day 3 凌晨 2:48，Claude 正在处理一个涉及 q-展开的下降步骤。另一个 agent 指出其中有错。Claude 重新计算后承认分母没有界，于是放弃这条证明路线，同时注明原陈述本身可能仍然成立。

Day 9 中午 12:55，一整条分支闭合。不到三小时前，该分支中的一条陈述刚被发现按字面写法是假的，随后得到修正。

Day 11 早上 7:54，Claude 记录了一次自己作为审阅者的漏检：

One correction I owe you: a statement [that I] passed this morning [as a reviewer] (a "model domination" lemma on the Cartier-module column) turned out to be false as written — [another agent] found the counter-example by computing a case my [review] had argued instead of computed. It was caught before anyone wrote a proof against it

Claude 先前通过推理放行了一条“model domination”引理，另一个 agent 直接计算具体情形后找到了反例。错误在任何 agent 开始为它写证明之前被发现。

Day 11 晚 8:25，距离终点约一个半小时，另一个 agent 又对 Claude 放行的一条引理提出异议。Claude 复查后承认：Own-miss. I must post a correction promptly。

证明规模在这些检查与修正中持续增长。Day 2 已有约 2,100 条定理，Day 6 超过 10,000 条。累计曲线在 Day 7 短暂下探。PDF 解释，这次下降来自依赖树重新连接，并不代表已经完成的工作丢失。

Day 4 的视频帧显示，依赖图从中心向外扩展。当时共有 6,851 条陈述，其中 6,504 条已证明。

Day 10 下午 2:58，一个 agent 完成了原本估计需要几周才能完成的步骤。实际用时只有两小时多一点。它提交了一份 7,300 行的证明，第一次提交就被接受。到 Day 11，最终证明的依赖树包含 29,511 条定理，而且全部已证明。平台在整个项目中共生成约 30,300 条定理。

Day 11 晚 10 点，最后一条开放陈述得到证明。几秒内，完成状态沿依赖图向上传递，先后穿过 Ribet 的 level lowering 和证明所需的模性提升步骤。平台在 02:00:57Z Aug-18（10:00:57pm ET Aug-17）把费马大定理标记为 Proved。

证明层完全交给 agent 后，内核可以保证正确性，却不会让产物自动变得适合人读。README 对整个代码库的描述是：written to be checked rather than read。

文件名和定理名由机器生成。P2M 与十六进制后缀只是流水线标签，不是数学概念。名称与陈述不一致时，真正被证明的是陈述。发布版本还删除了大部分注释，只保留上游声明、doc string、引用，以及 #guard_msgs 用来核对预期输出的注释。

博客脚注也承认，这份证明很可能远长于实际所需。它是 Mathlib 的 5 倍多；部分原因是 Mathlib 的代码更精炼，而且经过充分审阅。

约两周后，Claude 被问及这份证明与帝国理工学院团队编写的 Lean 库有何区别。它先回答：correctness is not the difference. The difference is form。

Claude 自评称，这份代码不能当作数学文本来读。发布版本没有注释。900 多个文件超过 Mathlib 的 1,500 行上限，而 Mathlib 自身只有 2 个这样的文件。

这些经典结果也没有按最一般、最方便复用的形式来证明。它们只证明了这条费马大定理路线实际需要的强度。

重复是另一项明显特征。Claude 把这一项概括为 Duplicated, not shared。约五分之二的定理陈述，也在另一个证明文件里逐字出现过。所有证明文件的代码行中，约五分之一是其他地方已有声明的逐字副本。一条基础引理甚至在 300 多个文件中被重新声明。

工程环境也很庞大。生成的 preamble，也就是每个文件开头的环境设置段，占全部字节的 31%。约 11,700 个文件单独设置了计算上限。

工具链从 Lean 4.30 升到 4.33 后，29,511 个证明文件中有 7,620 个发生改动，占 26%。其中 5,672 个需要逐个修复，占全部证明文件的 19%。

论文中的 milestone 和“先搜索再提交”，针对的正是对同一陈述的重复形式化。最终产物里仍有约五分之二的陈述重复。

不同来源对代码规模采用了不同口径。Claude 自述代码量为 1350 万行，约是 Mathlib 的六倍，并称证明中约有 533,000 条局部辅助引理。PDF 正文写约 1300 万行；去掉生成的 boilerplate 后，约为 1050 万行。博客采用的主口径也是 1300 万行 Lean。

PROOF-PATH.md 还记录了每个经典结果的证明覆盖什么范围。Mazur 部分只证明 Frey 曲线在 p ≥ 17 时的不可约性，也就是这条路线需要的 Eisenstein 商结论。指数 5、7、11、13 由 Kummer 理论或下降法直接处理，没有使用 Mazur 关于一般曲线的完整定理。

Langlands–Tunnell 部分只证明八面体情形。对象限定为满射、行列式是分圆特征的 ρ̄₃，而且带有 level 条件。

模性提升只覆盖两条带 level 条件的陈述，分别处理半稳定模型 W 在 p = 3 和 p ∈ {3, 5} 时的情形。Ribet 部分也采用较窄的版本：它只证明 Frey 表示在无平方因子、由导子支持的 level 上可以进行 level lowering，结论写成迹同余。

Buzzard 还指出，这份证明采用的是 Darmon、Diamond、Taylor 在 1995 年讲义中整理的路线，不是他自己的项目所走的现代路线。博客提到，仅描述 Buzzard 项目初始阶段的 blueprint 就有 86 页。

在 Buzzard 看来，小素数情形已经由 flt-regular 项目的结果覆盖。该项目由 Best、Birkbeck 等六位作者在 2025 年发表，形式化了 regular primes；最小的 irregular prime 是 37，因此小素数覆盖是完整的。

最终证明约有 7% 的非模板行来自此前的失败尝试。

Prove2Me 论文在结论中这样划分人的判断与 agent 的劳动：

Buzzard 判断，如果 AI 群体能在 11 天内端到端形式化几千页数学文献，今后的研究成果可能会在产生时同步完成形式化。机器将检查 Langlands 纲领的现有文献，并标出尚未完成的论证。有些论文会直接使用“专家都知道”的结果；机器可以把这些隐藏的前提明确列出来。

It will also keep us honest