费马大定理说，当n大于2时，xⁿ + yⁿ = zⁿ没有正整数解。皮埃尔·德·费马在17世纪30年代把它随手写在书页空白处；安德鲁·怀尔斯在20世纪90年代用史上最难的一些数学证明了它。2026年9月4日，Anthropic宣布Claude用11天完成了这一证明第一个完整的计算机验证版本[1]。本文解释这意味着什么，为什么它既是数学故事也是计算机科学故事，以及它并不意味着什么。
时间线
- 17世纪30年代费马声称有一个“这里空白太小写不下”的证明。
- 1994–95年安德鲁·怀尔斯（与理查德·泰勒合作）完成证明。
- 2024年Kevin Buzzard在伦敦帝国理工学院启动用Lean形式化该证明的人工主导项目。
- 2026年8月Claude智能体用11天完成完整的Lean形式化。
- 2026年9月4日Anthropic宣布成果；Buzzard进行审阅。
证明助手做什么
GCSE核心
人写的证明会把一些小步骤留给读者。即使是专家审稿人也可能漏掉漏洞。像Lean这样的证明助手消除了这种风险。你把定义和证明写成代码，一个小而可信的检查器（内核）确认每一步都由逻辑和此前的结果推出。如果代码能编译，定理就得到验证。它就像一个编译器：除非程序被证明正确，否则拒绝运行。
形式证明是一棵树：最终定理依赖于重要的中间结果，中间结果依赖于引理，引理又依赖于定义和基本事实。Lean检查每一条连接。按下按钮，从地基开始逐步检查这棵树。示意图；真实的树约有2.95万个定理。
Claude实际做了什么
A-Level拓展
- 它形式化了怀尔斯证明的一个简化版本，出自Darmon、Diamond和Taylor[1]。
- 成果约有1300万行Lean代码和约3.03万个定理（最终证明用到约2.95万个），是Mathlib的五倍多[1]。
- 数十个Claude智能体在11天里并行工作，使用了一个内部研究模型约60亿个输出词元[1]。
- 人类的数学投入仅限于Anthropic研究员Tianyi Peng偶尔给出的高层次指令[1]。
- 证明只依赖Lean的三条标准公理，一个比较工具确认最终定理的表述与Mathlib自己对费马大定理的表述完全一致[1]。
- 它复用了Kevin Buzzard在伦敦帝国理工学院FLT项目中的部分内容，Buzzard审阅了完成的证明[1]。
快速检测
证明在Lean中“编译通过”意味着什么？
为什么检查命题很重要
计算机验证的证明只有在证明了正确命题时才有用。如果定理在Lean中写错了一点点，对错误内容的完美证明就毫无价值。所以团队用比较工具确认命题与Mathlib中独立写出的版本一致；“没有额外公理”的检查也很重要：它表明没有任何东西被直接假定[1]。验证步骤和确认规格是两项不同的工作，和软件测试完全一样。
学生常常混淆的区别
正确不等于优雅（也不等于新）。
考试式问题
以费马大定理的形式证明为例，解释验证（verification）与确认（validation）的区别。 [4分]
显示范例答案与得分点
- 验证是检查产品是否构建正确，即是否符合其规格 (1分)
- 在这里，Lean验证证明的每一步在逻辑上都是正确的 (1分)
- 确认是检查是否构建了正确的产品，即规格是否符合实际需要 (1分)
- 在这里，把Lean中的命题与Mathlib中独立写出的FLT命题进行比较，检查证明确实证明了预期的定理 (1分)
考官关注的重点: 给出两个术语的定义，并把每个术语对应到例子的具体部分。
常见错误: 把这两个词当作同义词。程序可能通过所有验证检查，却仍然做错了事。
逻辑、证明和测试把A-Level数学与计算机科学联系在一起。我们的文章AI真的会做数学吗？描绘了更大的图景，而千禧年大奖难题展示了哪些问题仍悬而未决。
参考资料与延伸阅读
- Anthropic: Formalizing Fermat's Last Theorem (4 Sep 2026) — 规模、智能体、公理、人类投入、Buzzard审阅、注意事项
- AI Weekly: Claude formalized Fermat's Last Theorem in 11 days — 新闻报道
- Lean community: Mathlib — Lean数学库
- Imperial College London: Fermat's Last Theorem formalisation project (Kevin Buzzard) — 人工主导的项目
最后审校日期:2026年10月5日。以上数据为已公布的典型数值,规则可能会发生变化。考试用语因考试大纲而异,请以你所在考试局的规定为准。
常见问题
是AI证明了费马大定理吗？
不是：安德鲁·怀尔斯在20世纪90年代证明了它。2026年发生的是，Claude智能体把该证明的一个版本翻译成了Lean——一种其检查器会验证每一步逻辑的编程语言。Anthropic于2026年9月4日宣布的这一成果，是该定理第一个完整的计算机验证证明。
Lean是什么？
一种证明助手：在这种编程语言里，定义、定理和证明都写成代码。一个小而可信的程序——内核——检查每一步是否由逻辑规则和此前的结果推出。如果证明能编译通过，定理就得到了验证，前提仅是Lean内置的公理。
这个证明有多大？
约1300万行Lean代码，约3万个定理（最终证明用到约2.95万个），是Lean主要社区数学库Mathlib的五倍多。耗时11天，数十个Claude智能体并行工作，Anthropic研究员Tianyi Peng偶尔给出高层次的指导。
AI写的证明好吗？
从Lean已检查过它的意义上说，它是正确的；在伦敦帝国理工学院领导人工FLT形式化项目的Kevin Buzzard也审阅过它。但Anthropic表示，它很可能比需要的长得多，失败的尝试留下了约7%的非样板代码行。正确和优雅是两回事。
读者评分与评价
从多个维度为这篇文章打分——您的评价既能帮助其他读者,也能帮助我们不断改进。
这篇文章对您有帮助吗?
告诉我们您的想法——可以是需要更正的地方、尚未解答的问题,或您希望我们接下来讲解的主题。
想直接沟通吗？ 在方便的时间预约免费视频通话：简短问题15分钟，其他问题30分钟。时间以您所在的时区显示。
关于作者
Sudershan Soni
Mostak Services 的创始人兼首席导师——拥有硕士学位的数学、科学、计算机科学与 STEM 导师,拥有超过20年的职业经验,通过在线授课为全球从 11+ 和 GCSE 到 A-Level 及更高阶段的学生提供教学。
阅读完整履历