Claude 用 11 天完成费马大定理形式化：1340 万行 Lean，没有一处“显然”
2026 年 9 月 4 日，Anthropic 宣布完成史上第一个端到端、可由计算机完整验证的费马大定理证明。Claude 在几乎没有人工干预的情况下连续工作了 11 天，把安德鲁·怀尔斯的证明翻译成了 Lean 语言：1340 万行代码、约 3 万条中间定理，全文没有一处“显然可得”。数学界原计划用多年来完成的工程——伦敦帝国理工学院 Kevin Buzzard 负责的项目仅第一阶段技术蓝图就有 86 页——结果不到两周就画上了句号。
先说清楚一件事：这里并没有新证明。模型没有找到通往定理的新路径，它做的事情甚至更难——把一份人类写的、到处都是“由此平凡推得”的证明，改写成每一步都由编译器检查的形式。自 1995 年以来，数学家对怀尔斯证明的把握是 99.9%；现在可以放心说百分之百，因为整个推导链条都从 Lean 的三条标准公理出发跑了一遍，再无可疑之处。
计算机到底验证了什么
这里数字比形容词有用。
- 1340 万行 Lean 代码——是这套系统旗舰形式化数学库 Mathlib 的五倍还多。
- 共证明了约 3 万条中间定理，最终论证用到了其中约 29500 条。
- 在 96 核机器上编译这个仓库，耗时约是编译 Mathlib 的 20 倍；Buzzard 验证时拿到了一台 500 GB 内存的服务器。
- 整个证明只依赖 Lean 的三条标准公理，没有任何“为简化起见”的假设。
Kevin Buzzard 正是 2024 年起主持社区费马形式化项目的那位数学家。他下载了仓库、完成编译并运行了比对程序：最终定理陈述与 Mathlib 中的基准完全一致，全部检查通过。他的评价是“一次非凡的自动形式化成就”。
页边一行字，三百五十年的接力
1637 年前后，皮埃尔·德·费马在丢番图《算术》的书页边缘写下一个断言：当 n 大于 2 时，方程 aⁿ + bⁿ = cⁿ 没有正整数解。下面那句话成了传奇：“我发现了一个真正绝妙的证明，可惜这里空白太小，写不下。”从欧拉到库默尔，一代代数学家分块推进这个结果。1908 年，有人悬赏 10 万金马克征求证明，仅第一年就收到 621 份错误解答。
1993 年 6 月，安德鲁·怀尔斯在剑桥的系列讲座上公布了他的证明。两个月后，一位审稿人的提问暴露出其中一处构造的漏洞。怀尔斯花了一年时间修补——先独自尝试，再与前学生理查德·泰勒合作——一度几乎放弃，最终在 1995 年发表了这篇 129 页的论文。剩下最后一个“工程学”问题：能不能让计算机把这一切完整确认一遍？
不是新证明，而是新能力
此次形式化依据的是 Darmon、Diamond 与 Taylor 1995 年对怀尔斯–泰勒论证的阐述，途经 Langlands–Tunnell 定理和 Ribet 的水平下降定理。把怀尔斯证明形式化的想法早在 2000 年代就由荷兰计算机科学家 Jan Bergstra 提出，但直到不久前，这仍被视为一个领域许多年的工作量。部分情形——四次幂、正则素数——此前已移植进 Lean。随着新仓库的出现，Wiedijk 的 100 个形式化挑战——这个领域沿用二十年的基准——全部完成。
Buzzard 坦言：从数学本身看，这项工作没有告诉我们任何新东西——他本来就相信怀尔斯。价值在别处。如今验证一篇新的数学论文动辄数月甚至数年；如果机器可以“即时”把证明形式化，评审周期会大幅缩短，那些“专家都知道”式的隐藏假设也会浮出水面。对一个靠结论可靠性立足的学科来说，这是重要的转变。
这 11 天内部是什么样子
项目由 Anthropic 研究员田翼彭（Tianyi Peng）主导，他此前在哥伦比亚大学组建了 AI 形式化工具研究组。按他的说法，起初并没打算一路走到终点，只是想看看 Claude 能把 Buzzard 的项目推进多远——结果直接推到了终点。
大量智能体并行工作：有的补数学定义，有的攻坚中间引理，有的沿定理树向上推进，还有的把各部分重新拼装成完整论证。最初几天相当混乱——智能体把握不住项目全局，早期尝试的成果只有约 7% 保留进了最终代码。转折点是团队换上 Prove2Me 平台：证明在其中表现为定理节点组成的图，任何时候都能看清哪些已证明、哪些在等前置、下一步该攻哪里。定理陈述与证明分离管理，编译提速，每个定理还带有便于检索的文字描述。工程规模约为 60 亿输出 token，人类只给出“这个方向优先级更高”这类高层提示。
去哪里看
仓库已发布在 GitHub，如果你能找到一台 96 核机器，完全可以自己运行一遍验证。一手资料：Anthropic 的官方解读和 Xena Project 博客上 Buzzard 的文章。
看完 1340 万行的故事，如果你想看看现代模型处理小一些的任务——算法、代码、计算——的表现，欢迎到 NeuralSpace 的「代码」和「对话」板块试用，也可以通过 API 把模型接入自己的项目。