Claude完成费马大定理首个形式化证明：1300万行Lean代码创纪录

验证一个重大数学证明是否正确，往往需要耗费数年时间。而将数学推理转化为Lean等计算机证明助手可以验证的形式——即"形式化"（Formalization）——正在成为破解这一难题的新路径。近期，Anthropic的Claude完成了费马大定理（Fermat's Last Theorem）的首个形式化证明，这在数学界和AI界都引发了广泛关注。

一项曾被认为需要数年的工程

费马大定理是数学史上最负盛名的定理之一。它由费马在17世纪提出，直到1995年才由英国数学家安德鲁·怀尔斯（Sir Andrew Wiles）爵士给出完整证明——距离最初的猜想已过去350多年。

然而，人工证明的完成并不等于机器可验证。将怀尔斯的证明完整地翻译成Lean可以逐步核验的形式，是一项极其庞大的工程，此前多数专家认为这需要许多年才能完成。Claude此次的工作，正是把这个"多年项目"向前推进了一大步，并产出了迄今为止规模最大的Lean证明。

1300万行代码与2.9万个附属定理

根据Anthropic公布的信息，这份形式化证明总量超过1300万行代码，为机器验证提供了坚实基础。这一数字背后的意义远不止于"证明了费马大定理本身"。

更值得深挖的是，为了支撑主证明，这项工作还顺带证明了超过29,000个必要的附属定理，覆盖数学的多个此前从未被形式化过的分支领域。换句话说，这不仅仅是给一个著名定理"盖章认证"，更是在系统性地夯实数学知识核心的底层基础设施。

数学证明的复杂性决定了它往往依赖大量前置结论，而这些结论此前散落在纸面证明中、缺乏机器可验证的形式。此次一次性形式化近三万个定理，实际上为整个Lean生态和数学库Mathlib补齐了大量缺失的拼图。

建立在三个世纪与数百贡献者之上

Anthropic特别强调，这项成果并非凭空而来，而是建立在三个世纪数学家的积累，以及数百位Lean和Mathlib社区贡献者的工作之上。

这一表述点出了一个容易被忽视的事实：AI在数学形式化中的角色，是站在既有人类知识体系与开源工具链的肩膀上。Lean作为证明助手、Mathlib作为其数学库，本身就是全球协作的产物。Claude的贡献在于以远超以往的效率和规模，把这些分散的推理拼接、翻译并交由机器核验。

AI辅助验证能缓解数学审稿压力吗

这项工作指向一个更具现实意义的问题：在数学论文产出量前所未有增长的今天，同行评议的负担越来越重。审稿人需要花费大量时间逐步核对证明的正确性，而错误有时要在多年后才被发现。

Anthropic对AI辅助的数学证明验证持乐观态度，认为它有望减轻数学审稿的负担。如果机器能够对形式化后的证明给出可靠的正确性核验，那么人类专家就可以把精力更多地放在思想创新与结构性判断上，而非机械式的逐行检查。

当然，这里存在一个前提：把纸面证明转化为形式化证明本身仍是高门槛工作。AI能否在这一环节持续降低成本、提升可靠性，将决定这一愿景能走多远。

对AI能力边界的一次检验

从AI能力评估的角度看，费马大定理的形式化是一个极佳的"硬指标"。它不像自然语言任务那样存在评分主观性——Lean的验证结果是二元的：要么通过，要么不通过。这意味着这项成果的正确性有明确、可复现的标准。

Anthropic已将完整证明公开在GitHub上，并在其Science Blog中介绍了整个过程，任何人都可以查验。这种可验证、可复现的透明度，也正是数学形式化工作相较于许多AI"能力宣称"的独特价值所在。

结语

Claude完成费马大定理形式化证明，是AI在严谨数学推理领域的一个标志性节点。它既是规模上的纪录（史上最大的Lean证明），也是方法论上的探索——用AI加速人类数学知识的机器化与可验证化。在证明产出爆炸式增长的时代，这类工作或许会逐步改变数学验证的方式，让"检查一个证明是否正确"不再动辄耗费数年。