约1637年，皮埃尔·德·费马（Pierre de Fermat）在古希腊数学家丢番图所著的《算术》一书的页边空白处写下一个命题，后来成为史上最著名的数学猜想之一：当整数n大于2时，不存在满足aⁿ + bⁿ = cⁿ的正整数a、b、c。这个被称为费马大定理（FLT）的猜想极难证明，安德鲁·怀尔斯爵士在1995年给出的首份证明长达129页，且需要经过数月细致工作才能完成核验。

我们在此公开费马大定理的首个完整计算机校验证明：Claude 在 11 天里基本自主地用 Lean 语言写出了这一证明。以下介绍这次形式化的做法，以及它对研究数学可能意味着什么。

大约在 1637 年，皮埃尔·德·费马在丢番图《算术》一书的页边写下了一条断言，它后来成为数学史上最著名的猜想之一：对任何 n > 2，不存在正整数 a、b、c 满足 aⁿ + bⁿ = cⁿ。费马大定理证起来极其困难。安德鲁·怀尔斯 1995 年给出第一个证明，全文 129 页，数学界花了数月艰苦核验才确认无误。

十年后，荷兰计算机科学家 Jan Bergstra 提出把怀尔斯的证明“形式化”，也就是转成计算机能够自动检查的形式。此后数学家们一直在发展编码这种复杂证明的方法，其中包括伦敦帝国理工学院 Kevin Buzzard 牵头、2024 年启动的多年社区项目，目标是用 Lean 证明助手完成形式化。

最近，Anthropic 研究员、在哥伦比亚大学带领团队做 AI 形式化工具的 Tianyi Peng 想测试 Claude 能否推进 FLT 的形式化。结果远超他的预期：Claude 在 11 天内基本自主地产出了首个端到端、经计算机核验的 FLT 证明，沿途写下 1300 万行 Lean 代码，证明了 29,500 个中间定理。

Kevin Buzzard 评价说：

这一非凡的自动形式化成就——Anthropic 研究者说它只花了 11 天——在除数学公理外不作任何假设的情况下证明了费马大定理。其间，我们看到了代数、调和分析、几何和数论的自动形式化，也看到 AI 自动形式化的产物如今已足够可靠，可以在其上继续搭建；这个证明是多层次的。

能自动形式化像 FLT 这样复杂的证明，是迈向“数学结果都能被方便核验”的未来的一大步。随着 AI 产出越来越多证明，简便的形式化可以减轻评估新结果的负担——这一过程有时要花数年。我们希望，数学所依托的公共知识体系会变得更容易信任，而不是更难。

验证数学证明的挑战

与近来 AI 在黎曼猜想方面的工作不同——那是产生新数学——这里的新意在于“验证”：像用计算器检查计算一样用计算机检查数学证明。证明定理要组装起复杂的逻辑链，任何一环断裂，后面的结论都可能是错的。想把一个新结果理解到足以确信其正确，往往要花数月甚至数年。

FLT 就是现成的例子。费马在书页边写下定理，旁边附了一句诱人的话：“我发现了一个真正奇妙的证明，可惜这里页边太窄，写不下。”

此后三百五十多年，一代代数学家寻找 FLT 的证明。1908 年，有人悬赏 10 万德国金马克（约合今天一两百万美元）征求正确证明；仅第一年就收到 621 份错误尝试。

1993 年 6 月，怀尔斯在为期三天的系列讲座中展示了他认为是第一个正确的证明。几位数学家密集核查了两个月后，一位评审向怀尔斯提问，暴露出一个关键缺口。怀尔斯花了一年想补上它，先独自一人，后与他的前学生 Richard Taylor 合作。他几乎要放弃时，才意识到早先抛弃过的一个办法可以修复证明。

1995 年 5 月，怀尔斯发表了第一个正确证明；它所用的现代数学技术远超出费马时代。由于几个世纪都没能找到初等证明，数学界如今相信，费马自己所谓“奇妙的证明”很可能是错的。

检验证明是否正确的办法之一，是交给计算机。Lean 这类证明助手用算法核验证明的逻辑，能毫无疑问地确认其正确性。难的是人类要把证明改写成 Lean 能懂的形式：给人读的证明会跳过许多显然步骤，Lean 却要求每一步都写出来。人的证明还建立在数百年已发表成果之上，而形式化只能从已被形式化的那部分数学起步。

FLT 的形式化原本预计要花数年。数学界用来描述该项目初始阶段的蓝图就有 86 页。

Claude 在 11 天内完成了证明，沿途给 30,300 个定理写出了计算机可核验的证明（最终版本使用了其中 29,500 个）。几十个 Claude 智能体协作起来定义概念、证明中间定理，再借助它们去攻克更难的命题。整个证明有 1300 万行 Lean 代码，是它所依托的社区数学证明主库 Mathlib 的 5 倍以上。

Claude 的证明遵循 Darmon、Diamond 和 Taylor 对怀尔斯证明的简化版本。人类给出的数学输入只是 Tianyi 偶尔的高层指令，比如“Jacobian as a scheme 似乎是高优先级”“把 Mazur 定理尽快推完”。接近终点时，Claude 在自己的记录里写道：“FLT 根节点显示 PROVED。历史性时刻。”

最初的一些尝试其实失败了：智能体虽有早期成功，但很快就会丢失项目状态、协作失灵。这些失败尝试贡献了最终证明中约 7% 的非样板代码。

转机出现在改用 Prove2Me 之后。这是 Tianyi Peng 与哥伦比亚大学合作者设计的开放协作形式化平台，作用是：

1. 维护一张定理陈述的有向无环图（DAG），智能体据此决定接下来该证明什么，这有助于缓解记忆退化，也便于多个智能体并行工作。
2. 把定理陈述和证明分放不同文件，链接另立维护，从而加快 Lean 编译、减少资源消耗。
3. 为每条定理陈述维护一条自然语言描述，便于搜索和复用，简化了证明路径。

借助 Prove2Me 和基于 Claude Code 的多智能体框架，智能体团队用了不到两周完成证明，消耗大约 60 亿输出 token，模型是能力大致相当于 Claude Fable 5.1 的通用内部研究模型。Lean 核验了最终证明；它只用了 Lean 的三条标准公理，比较器也确认定理表述与 Mathlib 的 FLT 表述完全一致。

减轻形式化验证的负担

能有这种速度产出证明，说明如今已经可以形式化大范围的数学，这既能找出公共数学证明中的错误，也能减轻评审新成果的负担。看过 Claude 的 Lean 证明后，Kevin Buzzard 告诉我们：

如果 FLT 的自动形式化如今已经可能，我们就向现代数学文献的自动形式化迈出了一大步。这类技术将带来新工具，剔除当前数学文献中的错误，为评审者减负，也使我们能够严格核验 LLM 生成的数学——这项工作目前通常要靠人来做，代价极高。

对 AI 给出的数学结果，形式化也是人类建立信心的主要途径。随着 AI 和 AI 辅助的数学家产出越来越多证明，AI 辅助形式化能够替人工评审分担一部分工作。我们预计，今后面向人类读者的论文会普遍附上一份形式化证明。形式化证明不应取代人能读懂的阐述，但要跟上 AI 的产出数量，它可能是数学界唯一现实可行的办法。

写 Lean 似乎也帮助 Claude 证明新结果。Anthropic 最近不少由 Claude 完成的成果都是边证边形式化；Claude 会像用数值模拟确认推导方向那样，拿这些部分证明独立检查自己的假设。

形式化 FLT 是消耗 token 极多的项目，但它也是迄今最大的 Lean 证明。Anthropic 研究者做了一个小实验：用三份个人 Claude Max 订阅计划去形式化 Hardy–Littlewood 圆法的应用。智能体完全通过 Prove2Me 协作，仅用三天就完成了 Vinogradov 三素数定理的形式化。我们认为，只要脚手架得当，用消费级 AI 订阅协作形式化重大成果是可行的。

为此，Anthropic 和其他实验室最近都扩大了对外部研究者的支持，为做纯数学和形式化的数学家提供免费或折扣订阅及研究积分，Anthropic 也为更大规模的科学项目设有专项资助。

AI 正迅速改变数学研究的面貌，数学家们也在思考这对自身工作的意义。但至少对形式化，我们觉得 AI 的角色毫无疑问是正面的。随着形式化变得更常用，我们希望它能帮助数学公共知识体系维持住人们的信任。

评论区最统一的反应是“这下连 Buzzard 也被截胡了”：帝国理工 Kevin Buzzard 的团队本来就在做 FLT 的 Lean 形式化，结果被 Anthropic 抢先完成。随后共识迅速裂开：赞扬派把 1300 万行 Lean 和 29,500 个引理当作机器形式化能力的里程碑，质疑派则盯着仓库里 self-assessed 的标记，怀疑这是 AI 自己给自己签发的验收单。

认为这是形式化数学的里程碑

• 不少人联想到 Freek 100 清单，表示这个“重要定理是否已被证明助手形式化”的名单上又多了一个真正的硬骨头；也有人直接感叹这是最难形式化的证明之一，回应充满“Impressive”“Wow”式的震撼。（较多人）
• 有评论指出真正的意义不是“AI 又解出一道难题”，而是它说明现在可以快速形式化“大片数学”，让机器去查人类证明中的常见错误、替期刊审稿人分担负担；原文把这个重点放得太靠后了。（少数人）
• 也有人从规模读出更一般的结论：只要目标能被明确验证为正确，模型就有能力把它完整走完，无论这个过程多长多碎。（少数人）

这进一步支持了那个看法：任何能被证明正确的东西，模型都能做到。（@mw）

质疑“self-assessed”式的大规模自评

• 仓库的 formalization.yaml 里状态一栏写着 self-assessed，立刻成为靶子：这种自评离独立复核还差得远，尤其当代码量高达 1300 万行时，普通读者根本无从审起。（少数人）
• 另有人提出更技术性的担忧：如此庞大的证明会不会在某个角落利用了 Lean 或底层内核自身的漏洞？13M 行这个量级让“已通过内核检查”这句话的分量变得很可疑。（少数人）

1300 万行的状态写着“自我评估”；Lean 和 Nanoda 的内核有没有漏掉一个 Collatz 式的漏洞？真要复核，就把它翻译到 HOL-light 里试试，别出错。（@lseplot）

抱怨 Lean 可读性差：机器能写，人却读不进去

• 有读者说自己认真学过几何代数、李理论这些高等数学，但大脑依然“无法处理 Lean”；Isabelle 和 RCoq 给他的感觉自然得多，如果未来数学证明都由 Lean 书写，等于让机器在一种人类难以阅读的语言里自我表演。（少数人）

我读不了 Lean，它不是我想证明问题的那种方式。希望有人能发明更易于消化的证明语言。（@rao-v）

认为 AI 现在只会苦干，还缺 Wiles 式的灵光

• 有人承认 LLM 很擅长在已有框架里把巨量细节补完，但随即提出对照：它什么时候能做出 Andrew Wiles 那种没人指明方向的战略级突破？这条质疑和“模型什么都能做”的乐观论正好形成对峙。（少数人）

LLM 很擅长埋头苦干。可它们什么时候能做出 Wiles 那种真正的突破？（@drivebyhooting）

担心机器证明会抽走数学中的“人味”

• 有人把 Wiles 当年的证明过程描述成“近乎落泪的情感和精神体验”，觉得如果以后大定理都由机器完成，人类会失去这种对奇迹的切身感受；不过同一个人也承认，超越生物学极限的未来仍然值得期待。（少数人）
• 也有评论把问题推得更远：AI 显然有能力以更快的速度和更高的可靠性替代人类完成认知任务，真正的问题不是“能不能”，而是“社会允不允许它走到那一步”，以及那之后人类如何自处。（少数人）

认为这只是烧电的“AI 垃圾数学”

• 少数唱反调的人完全不吃这套：impressive 归 impressive，AI 做形式化证明既没改善普通人的生活，也没让地球更好，只是让富人更富、给极客发多巴胺，并烧掉所有人的电费。（少数人）

我们已经进入“垃圾数学”时代。它可以很惊人，但它让地球上谁的生活变得更好了？（@dakolli）

有价值的补充

• 有评论注意到项目使用了 prove2.me 这类协作工具，认为这比单条定理本身更值得玩味：未来 AI 要搞定大型研究任务，可能不只是靠更大模型，还要给 agent 配一套类似 JIRA 的项目管理和协作设施。
• 也有人用证明助手的口气开了一个很认真的玩笑：下一步是不是该执行 simplify，看这 1300 万行能不能瘦身一半？甚至未来会不会出现一个元定理，证明它已经无法再被简化？这个追问其实把“机器证明如何变成人能读的证明”摆到了台面上。
• Anthropic 同步放出了相关仓库，想亲自验证 self-assessed 争议的读者可以直接打开 formalization.yaml 查看状态声明。