Anthropic让Claude啃费马大定理：大模型开始深入Lean数学证明

Anthropic近日发布研究文章《Formalizing Fermat’s Last Theorem》，展示如何让Claude参与费马大定理的形式化工作。这不是“Claude独立证明了费马大定理”，也不是把一段自然语言证明丢给模型后自动生成可编译代码，而是一次更接近软件工程的尝试：由人类拆解数学路线，Claude负责理解定义、寻找引理、生成Lean证明草稿，再根据编译器错误不断修改。

形式化证明是把数学命题和证明步骤翻译成定理证明器能够检查的程序。 与论文中依赖人类阅读的自然语言证明不同，形式化证明必须通过Lean内核的类型检查；每个变量的范围、每个定理的前提、每次等式变形的合法性，都要在机器规则下明确写出。

这件事的价值不在于“AI会不会做小学数学题”，而在于它开始触碰现代数学中最难自动化的一层：把数百页、跨越多个分支的研究级证明，拆成可以由机器逐行验收的数学代码。

费马大定理为什么难到需要一套工程系统

费马大定理断言：当整数 n 大于 2 时，方程 xⁿ+yⁿ=zⁿ 没有正整数解。 这个命题由皮埃尔·德·费马在17世纪提出，直到1990年代才由安德鲁·怀尔斯完成证明。

表面上，它只是一个关于整数幂的方程；实际上，怀尔斯的证明并没有直接在这个方程上做有限步数的代数变形，而是把问题转移到椭圆曲线、模形式和伽罗瓦表示等现代数论对象上。证明链条中包含谷山—志村猜想的关键特例、Ribet定理、模性提升等复杂工具，最终形成一套跨越多个数学分支的理论结构。

怀尔斯在1993年首次公布证明后，同行花了大约两年时间检查，才发现其中一个关键环节存在缺口。这个缺口后来由怀尔斯与理查德·泰勒共同修补。这个历史细节说明，研究级数学证明即使由顶尖数学家完成，也可能因为隐含条件、引用范围或技术性跳步而出现问题。

Lean的作用不是替数学家提出证明思路，而是把证明变成一份不能靠“看起来合理”蒙混过关的程序。 如果某个引理没有满足前提，或者某一步从环上的等式错误地跳到了整数上的结论，Lean会直接拒绝编译。

Anthropic这次到底让AI做了什么

Anthropic的实验重点是让Claude进入Lean的交互式证明循环，而不是让模型一次性生成整篇Wiles证明。 这套循环可以概括为四步：

1. 人类把数学目标拆成相对独立的定义、引理和中间命题；
2. Claude根据自然语言目标、已有上下文和mathlib中的定理，生成Lean证明草稿；
3. Lean编译器返回具体的类型错误、未解决目标或缺失实例；
4. Claude读取反馈，调整证明策略、补充类型信息，再次提交检查。

这种工作方式与普通聊天式数学问答有本质区别。用户问大模型“证明某个定理”，模型可以给出一段逻辑流畅但无法验证的文字；在Lean环境里，模型必须面对一个更硬的反馈：代码要么通过内核检查，要么失败。

Lean编译器在这里相当于数学领域的单元测试系统。 大模型可以快速写出大量候选证明，但只有能够通过检查的代码才能进入结果集。模型的语言能力负责“提出可能的下一步”，Lean负责判断这一步是否真的成立。

Anthropic披露的工作也反映出，Claude并不是简单地补全几行语法，而是在尝试处理更高层的证明组织问题，包括识别需要使用的数学对象、匹配库中已有定理、处理类型类与代数结构、将一个大目标拆成更小的子目标，以及在编译失败后回退到另一条证明路径。

不过，这项工作仍然不能被表述为Claude独立完成了费马大定理的完整形式化。 费马大定理完整形式化需要覆盖非常庞大的基础设施和现代数论结果，很多关键内容本身仍在Lean生态中持续建设。Anthropic展示的是AI能够深入参与这条路线中的若干形式化任务，以及它在长程证明工程中的潜力，而不是宣布一个已经由模型端到端完成的数学里程碑。

为什么“能写Lean”比“会做数学题”更重要

自然语言数学的最大问题不是表达能力不足，而是证明中的隐含信息太多。 数学家通常会省略显然的类型转换、标准引理和边界条件；对人类读者来说，这种压缩提高了可读性，对机器来说却意味着大量必须补齐的形式细节。

例如，一句“由有限生成模的标准性质可得结论”，在人类论文中可能只占一行，但在Lean里可能需要明确：对象属于哪个环，模是否满足有限生成条件，使用的是哪一个版本的定理，等式两边是否处于同一类型，以及相关实例能否由类型类系统自动推导。

大模型在Lean中的优势，正好对应形式化数学最耗时的部分：搜索、翻译和补全。 数学家往往知道证明的大方向，却不愿意把每个基础步骤都手工编码。Claude可以根据目标尝试寻找相近定理，也可以把一段人类数学描述转化为Lean表达式，再利用错误反馈定位缺失的前提。

但它的短板同样明显。模型可能选择一个表面相似、实际不适用的引理；可能在多个同名定义之间混淆；也可能生成极长、脆弱、依赖偶然化简规则的证明。更严重的是，模型仍然可能在宏观层面误解问题，把一个看似相关的中间结论当成真正需要证明的目标。

因此，Lean并没有消除大模型的幻觉，而是把幻觉从“听起来像对的文字”变成“编译失败的代码”。这是一种非常有价值的约束，但它不能代替数学家的路线设计和结果解释。

mathlib是这场实验真正的基础设施

mathlib是Lean社区维护的开放数学库，收录了从基础代数、分析、拓扑到更高阶数学的大量定义、定理和证明。 如果没有这些现成积木，形式化研究级数学就必须从公理、集合、数系和基本运算开始重建，工作量会迅速失控。

Anthropic的实验说明，大模型的能力高度依赖这套库的成熟度。Claude并不是凭空“记住”全部数学，而是在已有定义和定理网络中搜索可复用结构。库越完整，模型越容易把自然语言目标映射到可调用的形式化组件；库越稀疏，模型就越需要同时扮演数学家、库设计者和Lean程序员。

这也是形式化数学与传统大模型基准之间的区别。一个模型在竞赛题上得到正确答案，并不意味着它能写出可维护的Lean证明；反过来，一个能够稳定完成形式化任务的模型，也未必能提出新的数学猜想。前者考察结果预测，后者考察在严格类型系统中的长期推理和工程协作能力。

与传统自动定理证明相比，Claude的角色变了

传统自动定理证明器通常擅长在明确的形式目标上搜索，而大语言模型更擅长从人类描述中恢复证明意图。 两者并不是互相替代，而是形成互补。

| 方案 | 主要输入 | 优势 | 主要限制 | |---|---|---|---| | Lean内核 | 已形式化的证明项 | 可靠、可重复、可机械验证 | 不负责提出证明策略 | | 传统自动证明器 | 结构清晰的形式目标 | 在特定逻辑或代数任务上搜索高效 | 对自然语言和长程规划能力有限 | | Claude等大模型 | 自然语言、Lean上下文、错误反馈 | 擅长翻译、检索、拆解和生成候选步骤 | 可能误选引理，长证明稳定性不足 | | 数学家 | 问题背景和宏观证明路线 | 能提出新概念、新策略和关键洞察 | 手工形式化成本高，容易遗漏细节 |

更现实的系统不是“让模型替代证明器”，而是让模型充当一个懂数学的开发者：它负责写草稿、查库、重构证明和解释错误；Lean负责最终验收；数学家负责决定证明是否值得做、抽象是否正确，以及形式化结果是否对应原始数学命题。

最大的瓶颈不是算力，而是形式化成本

费马大定理形式化项目的核心瓶颈是数学库和证明工程的积累，而不是单纯增加GPU数量。 语言模型可以在几秒钟内生成候选代码，但如果相关定义没有进入mathlib，或者目标所需的桥接定理尚未建立，模型只能不断绕路。

这也是为什么“AI形式化数学”很可能先改变数学协作方式，而不是立刻自动发现新定理。一个大型项目可以像软件工程一样被拆分：有人负责定义对象，有人负责基础引理，有人负责连接不同分支，有人负责审查抽象接口，AI则帮助每个参与者处理重复性的形式化工作。

这种协作方式与陶哲轩此前对Lean的判断一致：当所有贡献都能由编译器验证时，数学家不必完全依赖对合作者个人能力的信任。一个陌生人提交的证明，只要通过持续集成和内核检查，就可以作为整个项目的一部分被复用。

“形式化费马大定理”仍然要避免两个误读

第一个误读是把形式化当作发现证明。 形式化通常把已有数学转写成机器语言，虽然过程中可能暴露原证明中的隐含假设，也可能推动新的抽象，但它并不自动等于发现了新的数学思想。

第二个误读是把编译通过当作所有层面的正确。 Lean可以保证代码遵循其逻辑内核和所使用的公理，但项目仍然需要确认形式化陈述是否准确表达了原命题，依赖是否透明，是否误用了额外假设，以及代码能否在未来版本中维护。

这点在费马大定理上尤其重要。一个项目即使完成了某个特殊情形，例如正则素数情形，也不能直接等同于完成整个定理。相关研究《A complete formalization of Fermat's Last Theorem for regular primes in Lean》所对应的正则素数路线，是完整形式化工程的重要组成部分，但它与覆盖全部情形、重建Wiles证明所需的完整理论链条之间，仍然存在明显距离。

对AI开发者意味着什么

Anthropic这次实验最值得关注的不是一个单点榜单，而是大模型产品形态正在从“回答问题”转向“在可验证环境中完成任务”。 在代码生成领域，模型已经通过编译器、测试和静态分析获得反馈；Lean把同样的闭环推进到了数学证明。

对于开发者来说，未来真正有竞争力的数学模型可能需要同时具备四种能力：

• 语义理解能力：理解自然语言定理、定义和证明上下文；
• 形式化翻译能力：把人类表述转换为Lean中的类型、命题和证明项；
• 工具使用能力：能够检索mathlib、调用自动化战术，并处理编译器反馈；
• 长程规划能力：围绕一个大目标维护数十甚至数百个中间引理。

这比传统数学问答更像一个带有严格测试系统的智能编程任务。评价模型时，不能只看最终答案是否正确，还要看证明是否能编译、依赖是否合理、代码是否可读、失败后能否恢复，以及它能否在更换库版本或稍微改变目标后继续工作。

我们的判断：这是重要信号，但离“AI证明数学”还有距离

Anthropic把Claude推进Lean证明环境，本质上是在验证大模型能否成为研究级数学的工程助手。 这件事有意义，因为它把模型的语言能力连接到了一个可审计、可复现的验证系统；它的成果不再只是聊天窗口里一段无法核验的推理，而是可以交给Lean内核检查的代码。

但短期内，最现实的产出仍然是“加速形式化”，而不是“自动完成数学革命”。模型可以节省查找引理、补写样板证明和处理类型错误的时间，却很难独立承担Wiles证明那种跨领域、长周期、需要新概念的总体设计。

如果Anthropic后续能够公开更多可复现的Lean代码、任务规模、成功率、人工干预次数和失败案例，这项工作的技术含金量会更容易被判断。尤其值得关注的不是演示中最漂亮的一段证明，而是模型在连续数百个相互依赖的目标上能否保持一致，以及它能否把一次性生成变成稳定的证明代理。

截至2026年9月4日，AI参与费马大定理形式化更准确的表述仍然是：大模型已经能够深入参与Lean数学证明流程，但尚未取代数学家完成整套现代数论证明。 这条边界看似保守，却正是这项进展最重要的地方——AI正在从“会解释数学”走向“提交能被数学内核验收的数学代码”。

参考来源

1. Lean 4 官方 GitHub 仓库：Lean语言、编译器和定理证明内核的开源实现。
2. mathlib4 GitHub 仓库：Lean生态中规模最大的开放数学库，包含大量可复用的定义、定理与证明。
3. Imperial College London 的 Lean FLT 项目：围绕费马大定理相关数学内容开展形式化工作的开源项目，可用于了解该方向的代码化进展。
4. Anthropic Research，《Formalizing Fermat’s Last Theorem》：本文关于Claude参与费马大定理形式化实验的主要信息来源，文章发表于2026年9月。
5. 《A complete formalization of Fermat's Last Theorem for regular primes in Lean》：关于正则素数情形形式化进展的研究工作，帮助区分部分情形形式化与完整费马大定理形式化之间的差异。