Claude仅用11天便形式化了费马大定理

原本需要数年的项目，为何仅用11天

伦敦帝国理工学院的数学家凯文·巴扎德（Kevin Buzzard）于2024年启动了一个将费马大定理形式化的项目。他最初的规划文档就有86页长。最初的时间预估是：需要一支由专家级数学家和形式化验证人员组成的团队投入数年时间。

Anthropic的Claude在11天内完成了同样的任务。

这项成果于2026年9月4日公布，其意义远超标题数字所呈现的内容。Claude生成了约1300万行Lean 4代码，验证了33000个定理，并在最终证明中引用了约29500个定理。这些代码规模超过Mathlib的五倍——而Mathlib是标准的Lean数学库，凝聚了人类数十年来将现代数学编码为计算机可校验形式的全部努力。

作为参照，安德鲁·怀尔斯（Andrew Wiles）原始的费马大定理证明仅有129页。人类团队逐行审阅这一证明、排查漏洞就需要数月时间。而将该证明形式化——即将数学推理转换为计算机可校验的语言——则是另一种完全不同性质的工作。每一个对人类读者而言"显而易见"的步骤，都必须在Lean中明确写出。这正是巴扎德的项目预期耗时数年的原因。

Claude究竟是如何做到的

关键并非简单调用一次Claude然后等待。数十个Claude智能体并行工作，各自负责定义、中间引理以及最终较难的综合命题。但仅靠并行化几乎未能成功。

Anthropic研究员、长期研究AI驱动数学形式化的彭天一（Tianyi Peng）描述了早期的尝试：智能体往往会丢失对整个项目状态的把握。缺乏协调的情况下，每个智能体都不清楚其他智能体的进展，导致工作停滞。

解决方案是Prove2Me——彭的团队专门为这类工作开发的协作平台。该系统将定理表示为有向无环图，使得每个智能体都能清晰看到哪些依赖关系已被满足、哪些目标尚未达成。系统还将定理声明与证明分离到不同文件中，从而加快编译速度。每个定理都附有自然语言描述，便于检索和复用已有结果。

这一基础设施细节至关重要。那1300万行代码不仅仅是原始生成量的体现——它们反映了一种组织集体形式化验证工作的全新方式。若按人类的传统方式推进，巴扎德的计划将是一系列定义与引理的线性序列。而Claude的方法则是分布式的、由图结构管理的、迭代的。

证明确实经过了验证

这项工作之所以需要反复核查，原因正在于此。在形式化验证中，一个错误的前提会像多米诺骨牌一样传导至所有基于它构建的内容。早期AI生成的数学内容有时会在大量后续工作完成后才暴露出其中的错误。

费马大定理的证明通过了Lean自身内核的检查，没有任何开放目标或未解决的子目标。它仅依赖Lean的三个标准公理。证明中不存在临时占位符——那种在Lean项目中标记未完成证明的 dreaded sorry 命令。另一个独立实现的内核nanoda（用Rust编写）也对超过一百万条声明进行了无误差验证。比较工具确认，该形式化表述与Mathlib中现有的费马大定理描述完全一致。

整个证明已在Anthropic组织下的GitHub仓库公开。任何安装了Lean的人都可以加载它并自行运行检查。

这对数学意味着什么

最直接的启示并非AI如今能够解决费马大定理——怀尔斯早在1990年代就已解决了它。真正的启示在于：AI现在能够将已有的证明转化为机器可校验的形式，速度之快超越任何人类团队此前所达到的水平，且规模远超以往任何尝试。

巴扎德自己的工作一旦完成，也将是一项里程碑。人类形式化验证者在重大定理上已取得令人印象深刻的进展，但进展依然缓慢，因为瓶颈本质上仍是人类——阅读、理解、重新表述、校验。Claude并未取代对严谨性的需求。它取代的是瓶颈。

这带来了一种张力。随着AI生成越来越多可形式化的证明，人类去验证它们的责任也在加重。Anthropic预测，未来计算机验证的形式化版本将与人类可读的论文一样成为标准做法。这将是数学生产与验证方式的一场结构性变革。

这也引发了一个关于署名与归属的问题：当一项证明由分布式AI智能体而非某位具名的数学家来完成形式化工作时，数学界的作者文化将意味着什么？巴扎德为此项目规划了数年，Claude仅用11天便完成。证明是同一个证明。区别在于谁将为使其成为机器可校验版本而获得署名——以及这种区分在未来的岁月里是否还会那么重要。

真正的里程碑

费马大定理举世闻名，但它并非最难证明的定理。这项成果的意义不在于定理本身，而在于规模。一千三百万行经过验证的Lean代码。三万个定理。一个由图结构规划工具协调的分布式智能体系统。所有这些成果在不到两周内完成。

以往的大型形式化项目——比如奇阶定理的证明——需要多年时间由专家团队完成。此次公告表明，这些时间线如今正被一个新的基准所衡量。数学界面临的问题已不再是AI能否形式化重大定理，而是人机速度差距将如何迅速缩小，以及当验证的成本低于直觉时，数学实践将发生怎样的变化。