费马大定理，终于有了一份能由计算机从头检查到尾的完整证明。
就在刚刚，Anthropic 声称，Claude 在 11 天内完成整个工程，写下约 1300 万行 Lean 代码，过程中人类只提供了少量高层指导。
完整的证明请参见 GitHub：
https://github.com/anthropics/fermats-last-theorem
这次 Claude 没有提出新的证明路线，它所做的是把已有证明转写成机器能够逐步核验的形式，让每一个逻辑环节都接受计算机检查。
对于费马大定理这样的世纪难题，此前数学界普遍预计，完整的形式化工程需要数年时间。
为什么费马大定理还要再「证明」一次？
1637 年前后，法国数学家皮埃尔・德・费马在《算术》一书的页边写下一个判断：当整数 n 大于 2 时，不存在满足 aⁿ+bⁿ=cⁿ的正整数 a、b、c。
他还留下一句：自己已经找到了一个「绝妙的证明」，只是页边太窄，写不下。
此后的 350 多年里，一代代数学家不断尝试。1993 年，安德鲁・怀尔斯在三场讲座中公布证明。两个月后，审稿人发现其中存在关键缺口。怀尔斯与理查德・泰勒又花费近一年完成修补，最终于 1995 年发表长达 129 页的完整证明。
费马大定理从此有了公认答案，但验证大型数学证明仍高度依赖人类。
数学论文通常会省略显而易见的步骤，也会直接调用前人已经建立的结论。面对一条跨越多个领域的复杂证明，审稿人需要逐层追踪它依赖的定义、定理与推导。整个过程往往持续数月，甚至数年。
形式化证明给出了另一种检查方式。
研究者先把自然语言中的数学推理写成 Lean 等证明助手能够理解的代码，Lean 再依据明确的公理和规则，逐步检查逻辑是否成立。人类可以略去的步骤，在这里都要补全。
2005 年前后，荷兰计算机科学家 Jan Bergstra 提出将怀尔斯的证明形式化。2024 年，帝国理工学院数学家 Kevin Buzzard 又发起了一项长期社区工程，尝试用 Lean 完成这件事。仅项目第一阶段的技术蓝图就有 86 页，原定周期以年计算。
11 天，3 万多个定理，1300 万行代码
Anthropic 研究员 Tianyi Peng 最初只是想测试，Claude 能否推动这项工程继续向前。结果很快超出预期。
Claude 沿用了 Henri Darmon、Fred Diamond 和 Richard Taylor 整理的一版简化证明路径。这条路线建立在怀尔斯证明之上，涉及代数、调和分析、几何和数论等多个领域。
数十个 Claude 智能体同时参与，它们定义数学概念，证明中间命题，再把这些结果组合成更高层的结论。整个过程中，Claude 一共完成 30300 个定理的机器可验证证明，其中 29500 个进入最终版本。
人类提供的数学输入很少。Peng 偶尔会给出「雅可比簇作为概形的优先级很高」、「尽快完成 Mazur 定理」等方向性提示，具体推导主要由 Claude 推进。
最终工程达到约 1300 万行 Lean 代码，规模超过 Lean 核心数学社区库 Mathlib 的 5 倍。整个任务消耗约 60 亿个输出 Token，使用的是一款能力大致相当于 Claude Fable 5.1 的内部通用研究模型。
完成后的证明由 Lean 检查，它只使用 Lean 的三条标准公理。一个针对 Lean 证明的比较工具也确认，Claude 所证明的定理陈述与 Mathlib 中的费马大定理陈述一致。
克劳德・怀尔斯 (Claude Wiles) 用 Prove2Me 计划形式化费马大定理的关键里程碑。图中三个彩色部分分别对应克劳德在最终目标实现过程中必须证明的三个核心子定理。该图与怀尔斯最初的证明过程非常吻合。
1300 万行这个数字也暴露出当前方法的局限。Mathlib 经过长期维护，代码紧凑、审查充分，Claude 生成的证明很可能远长于实际需要。它首先解决了「能否完整验证」的问题，距离简洁、优雅和便于人类阅读仍有很大空间。
几十个智能体，怎样完成一项长期数学工程？
这项工作一开始并不顺利。
早期实验中，多个 Claude 智能体很快失去对全局进度的掌握。它们不知道哪些命题已经完成，也难以有效复用彼此的结果，协作随之停滞。最终证明中约 7% 的非模板代码，仍来自这些失败尝试。
转折点来自 Prove2Me。这是 Peng 及其哥伦比亚大学合作者开发的开放式数学形式化协作平台。
Prove2Me 把待证明的定理组织成一张有向无环图，每个节点代表一项任务，节点之间记录依赖关系。智能体可以据此判断下一步该证明什么，也能在长时间运行后重新找到当前进度。
平台还将定理陈述与具体证明拆分到不同文件中，再独立维护二者之间的连接，这样可以缩短 Lean 的编译时间，减少计算资源消耗。每个定理同时配有自然语言描述，方便智能体搜索和调用已有结果。
在 Prove2Me 和基于 Claude Code 搭建的多智能体框架支持下，整个任务才真正形成稳定的协作流程。一个超长证明被拆成大量边界清晰、可以并行推进的小问题，局部结果持续汇入依赖图，最终一路连接到费马大定理的根节点。
这也是此次工程中更具普遍意义的一点。模型能力决定单个任务能走多远，外部脚手架决定几十个智能体能否在数天内围绕同一目标持续协作
AI 能证明，但谁来「证明 AI 证明对了」？
费马大定理早已有正确证明，因此，这次进展的价值主要落在验证环节。
Kevin Buzzard 在审阅后认为，这项成果说明，AI 自动形式化已经能够处理现代数学文献中的大型工程。相关工具可以帮助发现现有证明中的错误，减轻审稿人的负担，也能严格检查大模型生成的数学结果。
随着 AI 参与数学研究，证明的产出速度可能迅速提升。人类审稿能力却很难同步扩张。如果每一项结果都需要研究者从头检查，验证很可能成为新的瓶颈。形式化证明可以提供一份机器可核验的版本，让审查者把更多精力放在核心思路、理论价值和潜在影响上。
机器验证也有清晰的边界。Lean 能够确认一条逻辑链是否从给定公理正确推出结论，却不会自动给出直觉清晰、适合人类理解的解释。未来的数学成果很可能同时需要两套表达：一套写给研究者，讲清思路与意义；一套交给证明助手，确保每一步都经得起检查。
Anthropic 还进行了一次规模更小的实验，研究人员使用三个个人版 Claude Max 账号，通过 Prove2Me 协作，只用三天便完成了维诺格拉多夫三素数定理的形式化。这说明，类似工作未必长期局限于大型实验室，只要任务拆解和协作机制足够成熟，普通研究团队也可能参与其中。
这一次，Claude 没有解决一个尚未攻克的数学猜想。它让 AI 进一步进入数学知识的验证流程，也让大规模自动形式化第一次展现出接近工程化落地的可能。
参考链接：
https://www.anthropic.com/research/formalizing-fermats-last-theorem
https://github.com/anthropics/fermats-last-theorem
热门跟贴