Claude用Lean形式化费马大定理,11天写出1300万行证明

Anthropic于2026年9月4日宣布,其人工智能Claude完成了费马大定理的首个从头到尾均可由计算机验证的证明。该定理指出,当整数n大于2时,不存在满足a^n+b^n=c^n的正整数a、b、c。数学家安德鲁·怀尔斯于1995年发表了长达129页的证明,三十多年过去,此前从未有人对其逻辑进行过完整的机器验证。Claude在近乎自主的状态下工作了11天,用证明助手Lean编写了约1300万行代码。

该项目由Anthropic研究员、专注于AI数学形式化研究的彭天翼(Tianyi Peng)主导。在此过程中,Claude以计算机可验证的形式证明了约3万300条中间定理,其中约2万9500条被实际用于最终证明。生成的代码量超过Lean社区数学库Mathlib的5倍以上。数十个Claude智能体并行工作,分别定义概念、证明中间定理,再逐步攻克更难的命题。早期尝试曾多次失败:各智能体逐渐无法掌握项目整体进度,难以有效复用彼此的成果。最终证明中约7%的非样板代码正是源自这些失败的尝试。

什么是计算机验证的形式化证明

面向人类读者的数学论文往往会省略被认为"显而易见"的步骤。而像Lean这样的证明助手做不到这一点:无论多么琐碎的步骤都必须被完整写出。将已有证明改写成这种形式的工作被称为"形式化"。由于逻辑链条上哪怕一处断裂,都可能使后续所有结论失效,一份形式化证明只有在通过Lean的机器检查后,才能获得独立于人工复核的正确性保证。Claude的证明仅依赖Lean的三条标准公理,完全没有使用"sorry"——那种可以暂时跳过某一步证明的占位符。一个比对工具确认了Claude所证明的命题与Mathlib自身对费马大定理的表述完全一致,而一个用Rust独立编写的Lean内核"nanoda",也对超过100万条声明进行了无错误检验。

为什么费马大定理是如此具有象征意义的案例

这个定理得名于法国数学家皮埃尔·德·费马大约在1637年在丢番图《算术》一书页边空白处写下的一句话,他声称自己发现了"一个真正美妙的证明",但页边空白太窄写不下。此后350多年间,一代又一代数学家苦寻这一证明而不得。1908年,有人悬赏一笔相当于今天一两百万美元的奖金征求正确证明,仅第一年就收到621份错误的证明。1993年6月,安德鲁·怀尔斯在为期三天的系列讲座中宣布了自己的证明,但约两个月后,审稿人在复核过程中发现了一个关键漏洞。怀尔斯与他的前学生理查德·泰勒耗费近一年时间才修正了这个漏洞,并于1995年5月发表了最终版本——长达129页,数学界花了数月时间才完成验证。对国际读者而言值得一提的是,支撑怀尔斯证明的谷山-志村猜想,正是由日本数学家谷山丰与志村五郎在20世纪50年代提出的。而Claude此次形式化的,是达尔蒙(Darmon)、戴蒙德(Diamond)与泰勒(Taylor)提出的怀尔斯证明简化版本。

这项非凡的自动形式化成果,据Anthropic研究人员称仅耗时11天,在没有任何超出数学公理的额外假设下证明了费马大定理。在此过程中,我们看到了代数、调和分析、几何与数论的自动形式化,也了解到AI产出的自动形式化成果如今已足够稳健,可以在其基础上继续构建——这份证明是多层次的。

• 工作时长:11天,基本自主完成
• 生成的Lean代码:约1300万行,超过Mathlib的5倍以上
• 证明的定理数量:约3万300条,其中2万9500条用于最终证明
• 消耗的输出token:约60亿,使用与Claude Fable 5.1相当的通用研究模型
• 所依赖的公理:仅Lean的3条标准公理,零使用"sorry"

Claude究竟做了什么,又存在哪些局限

需要明确的是,Claude并不是独立"发现"了怀尔斯的原始证明。数学推理本身是怀尔斯及其合作者在1995年建立起来的;Claude所做的工作,是把这一推理的简化版本改写成Lean能够验证的严格符号形式,再交由机器进行核查——这是"形式化",而不是"发现"。这与近期AI在黎曼猜想上的研究性质不同,后者旨在产出全新的数学成果。Anthropic明确表示,这项工作的创新之处在于验证,而非发现。整个项目依托了由彭天翼开发的数学形式化协作平台Prove2Me,该平台以有向无环图管理各定理之间的依赖关系,使多个Claude智能体能够知道接下来该攻克哪条定理。人类的介入仅限于彭天翼给出的高层次指令,例如"应优先处理作为概型的雅可比簇"。

随着AI能够产出越来越多的数学证明,由人工逐一核验的负担也在加重。Anthropic预计,未来在面向人类读者的论文之外,同时提供一份可由计算机验证的形式化证明将变得越来越普遍。自2024年起主导一个多年期社区项目、在帝国理工学院用Lean形式化费马大定理的凯文·巴泽德(仅项目初期的工作蓝图就已达86页)将这一成果称为迈向现代数学文献自动形式化的重要一步:它有助于揪出现有数学体系中的错误,减轻审稿人的负担,并能够严格核验由AI生成的数学内容。

对中国的科技企业而言,这件事的意义并不止于一次数学层面的壮举。用于验证这一定理的证明助手,同样已被用来验证密码学协议、编译器正确性以及航空航天、芯片设计等领域的关键代码——而这些正是国内高校与科研机构近年来持续投入形式化方法研究的方向。一个AI智能体能够在数天内、而非数年内产出数百万行经机器核验的证明,这是一个具体的信号:长期以来被认为过于缓慢、过于专业而难以规模化的形式化验证,或许会变得更容易被纯数学领域之外的工程团队所使用——前提是,正如Anthropic自己所强调的,这种验证能力绝不能被误认为是自主发现新数学的能力。