9月4日，Anthropic宣布，研究员彭天翼推动的Claude项目用11天完成了费马大定理首个端到端机器核验的形式化证明。这个曾被预计需要多年推进的工程，如今生成了约1300万行Lean代码。项目公告

这项成果首次让完整证明链条接受计算机检查，其创新主要在验证方式，不能解读为AI用11天重新发现了怀尔斯的数学突破。

如何让古老难题接受机器核验

费马大定理断言：当整数n大于2时，xⁿ＋yⁿ＝zⁿ不存在正整数解。怀尔斯的证明及其与理查德·泰勒合作的补充论文于1995年发表，终结了三个多世纪的探索。

证明的关键，是将整数方程转化为椭圆曲线问题：排除已知的小指数情形后，假设存在反例，便能构造一条特殊的“弗雷曲线”。里贝特的定理意味着它不可能具有模性，怀尔斯的工作却保证这类半稳定椭圆曲线必须具有模性。

模性将椭圆曲线与具有高度对称性的模形式联系起来，两条结论发生矛盾，反例便被排除。证明综述

Claude沿用了达蒙、戴蒙德和泰勒整理的证明路线，将论文中默认读者能够补齐的推理展开，并为尚未形式化的数学工具编写证明。这需要将代数、几何、调和分析和数论中的复杂工具，连接成可核验的推导。

据技术报告，系统产出约3.03万条定理，其中29511条进入最终证明；成功运行期间，人类主要提供优先级等高层指导。技术报告

数十个智能体通过Prove2Me平台分工，平台记录定理之间的依赖关系，让模型知道哪些基础结果已经完成、下一步可以证明什么。共享进度、检索旧成果和复用证明，使漫长推导能够持续衔接。平台论文

这11天建立在长期积累之上：项目使用了Mathlib数学库，并改编了帝国理工费马项目及已有正则素数形式化项目的106个文件。技术报告

可信度来自对输出的独立检查：公开代码显示，证明通过Lean及另一个独立实现的内核核验，只依赖Lean的三个标准公理。核验还确认最终命题与Mathlib中的费马大定理表述一致，没有以未证明的占位符跳过难关。公开证明

专家看重的，是数学如何获得信任

英国帝国理工数学家凯文·巴扎德在9月4日的博客中确认，他亲自编译代码并运行核验工具，结果通过。他认为，这证明了大规模自动形式化的能力，但从数学思想看，成果基本忠实于已有文献。

巴扎德尤其期待，此类工具能够揭示论文中被“专家都知道”掩盖的隐含假设，减少审稿者逐层追查证明的负担。巴扎德评论

更广泛的学术讨论也提示，验证之后仍有工作。美国加州大学洛杉矶分校数学家陶哲轩此前将数学工作分为生成证明、验证证明与消化理解，强调解释关键思想、连接既有文献和未来方向的重要性。陶哲轩演讲

用这一框架衡量，机器核验提速之后，人类能否理解、压缩并推广证明，仍决定成果能产生多大影响。

工程成本同样值得关注：此次运行消耗约60亿输出词元，代码量超过Mathlib五倍。Anthropic承认代码可能远比必要的更长，因此文本规模不能等同于新增数学知识的规模。项目公告

这次突破展示了一种可能：未来数学论文可以附带可重复检查的证明凭证，让人类或AI提出的结论接受同样明确的逻辑审查。其价值最终将体现在研究者能否更快发现错误、复用可靠成果，并把精力投入新的数学问题。