你交给同事一份复杂报表，最难回答的往往不是“结论是什么”，而是“每个数字都核过了吗”。数学也一样。论文里的“显然可得”，在人类专家眼中或许足够；计算机却要求每一步都有依据。Anthropic这次让Claude把费马大定理写成Lean可以逐项检查的代码。值得看的不只是名题本身，而是一套让大模型持续工作、彼此协作，又不能绕过验证器的流程。
费马大定理说，当整数时，不存在正整数满足：
Andrew Wiles在20世纪90年代完成人类证明。Claude没有找到新路线，而是主要沿用Wiles与Taylor–Wiles的经典路线，把所需特例中的Mazur定理、Langlands–Tunnell定理、模性提升和Ribet降层等深层结果也写进形式化体系。所谓形式化，就是把论文中省略的步骤展开成精确的逻辑链。Lean既是编程语言，也是交互式定理证明器：Claude负责写，Lean负责逐行判定推导是否合法。
据Anthropic披露，Claude大致自主运行11天。人类偶尔调整任务优先级或给予鼓励，没有编写数学内容；除目标定理的一行陈述外，也没有编写Lean代码。这里的“首个”仍是Anthropic的发布口径，更稳妥地说，它公布了首个端到端、可由计算机完整检查的Lean形式化版本及复核文件。
真正的难点，是别让协作失控
一个模型很难把如此庞大的证明一次装进上下文。项目因此同时运行多个Claude Agent——可以理解为各自处理一块工作的AI协作者。有的写定理陈述，有的证明中间结论，有的互相审查，再把成果接回总工程。
早期尝试很快暴露问题：局部成果越来越多，Agent却不再清楚谁依赖谁。最终成品中，来自这段早期协作的非模板代码只有约7%；这一比例与项目约消耗60亿输出Token、内部模型能力大致相当于Claude Fable 5.1的说法，目前都只见于量子位对Anthropic材料的转述。
转折点是基于Prove2Me的multi-agent harness。Harness是包在模型外面的工程脚手架：它拆分任务、保存进度、调用Lean检查，并把错误退回给模型。Prove2Me又把证明组织成依赖图。每个定理像施工计划中的一个节点，前置工作完成后，后续任务才能接上。这样，超长证明不必由单个模型从头记到尾，而能分块推进、搜索和复用。
平台收尾时约有30,300个定理节点，最终证明实际依赖并重新检查了29,511个。另据量子位，证明文件中还有约533,000个辅助引理。代码规模约为1300万行，去除自动生成的样板后约1050万行；Anthropic文档另一处写作1350万行，因此这里只能视为不同统计口径，而非一个精确数字。
裁判不是Claude
这项工作的可信度不靠模型宣布“证完了”。完整工程被放进一个Lean项目重新编译，而且不含sorry——Lean里用来暂时跳过证明的占位符。它只依赖propext、Classical.choice和Quot.sound三个标准公理。
项目还用comparator与nanoda两个外部检查工具复核。comparator确认，最终命题与事先指定、能够导出Mathlib中FermatLastTheorem的命题一致。Mathlib是Lean的核心数学库。这一步防的是另一类错误：模型可能证明了一件逻辑成立、却悄悄偏离原目标的事。
证明也不是从空白开始。它复用了Mathlib、Imperial College London的FLT项目和flt-regular成果；据量子位转述，其中106个文件改编自后两个项目。代码行数据称达到Mathlib的约5至6倍，但Anthropic也提醒，原始行数受自动生成内容影响，不能直接等同于“包含更多数学”。
为什么这比再证一次名题重要
形式化数学过去最费人的地方，是把专家默认会补齐的细节全部写出来。Claude展示的变化，是把大模型、严格验证器和任务管理脚手架接成一条生产线：模型可以犯错，Lean即时拒绝；Agent可以忘记全局，依赖图替它保存工程状态；最后还能从目标命题到全部依赖重新检查。
Anthropic还讲过项目负责人Tianyi Peng的一段经历。本科时，导师准备把他的结果写入一篇Nature文章，临门前问他能否保证长证明正确。他只能说自己有99%的把握，最终错过署名机会。多年后，他主导的项目试图消除的，正是剩下那1%的不确定性。这里最有价值的变化，不是AI取代数学判断，而是机器生成的工作终于被放进一套可追踪、可拒绝、可重跑的审计流程。
局限与未知
- 这不是新的费马大定理证明路线，核心贡献是翻译、组织和验证既有数学。
- “首个完整形式化证明”带有发布方的营销色彩；现有两个载体也不等于已经完成两次独立复现。
- Anthropic承认，论文展示的Claude推理摘录所含数学说法没有逐条独立验证；当前代码也尚未达到Mathlib可接收的工程质量。