三百年才被证出来的数学题，AI 用 11 天写完 1300 万行代码，机器验过一遍

11 天、1300 万行：这次到底做完了什么

2026 年 9 月 4 日，Anthropic 发了一篇文章。Claude 用 11 天、基本靠自己，给费马大定理（Fermat's Last Theorem，简称 FLT）写出了一个形式化证明。这份证明能被电脑完整检查，语言为 Lean。Anthropic 把这个成果称为「FLT 的首个完整计算机可核查证明」。

先解释两个词。费马大定理是 1637 年费马写在书页边上的一个断言：n 大于 2 时，找不到正整数 a、b、c 满足 aⁿ + bⁿ = cⁿ，三百多年里无数人试过。Lean 是一款检查证明的软件，它只认写清楚的每一步推理，不认「显然」这两个字。

这件事的起点很随意：Anthropic 研究者 Tianyi Peng 本来只想试试 Claude 能走多远，结果远超他的预期。所谓端到端，就是从数学公理出发，到最后那句结论，每一步都被检查过。成品是 13,000,000 行 Lean 代码；一路上 Claude 证明了 30,300 个定理，最后那份证明用到了其中 29,500 个。

11 天是什么概念？数学界为这件事编的施工蓝图，光描述第一阶段就有 86 页；2024 年 Kevin Buzzard 在帝国理工学院发起的那项社区工程，是打算按年做的。Claude 这边的日志里，8 月 18 日 02:00:57Z 根目标被标记为 PROVED，同一句后面还留着一句「待复查」。

人类在这件事里说的很少，数学输入被限定为偶发的高层指令，比如「把 Jacobian 当作概形来处理听起来优先级很高」。证明本身也不是新路：它沿用的是 Darmon、Diamond 和 Taylor 对怀尔斯证明的简化版本。所以这次的新意不在数学，而在验证。Anthropic 特意把它与此前让 AI 做黎曼假设的工作分开：那一次产出的是新数学，这一次产出的是「可以反复运行的检查」。

一份证明为什么非要让机器再验一遍，人读了三百多年不算数吗？

过去三百多年，证明对不对都得靠人读

1637 年，皮埃尔·德·费马（Pierre de Fermat）在丢番图《算术》的页边写下那个断言。他还补了一句让后人争论三百多年的话：他有一个真正奇妙的证明，只是页边太窄，写不下。

1908 年，有人为这道题设下 10 万德国金马克的奖金（Anthropic 称约合今天的 100 万到 200 万美元）。光公布的第一年，就收到 621 份错误证明。

真正证出来的是安德鲁·怀尔斯（Andrew Wiles）。1993 年 6 月，他用三场连续的讲座公布了自己认为正确的证明，数学界一度以为大功告成；约两个月后，一位审稿者的提问让它暴露出一个关键缺口。怀尔斯先独自修了一年，再和前学生理查德·泰勒（Richard Taylor）合作，在快要放弃的时候想起一个自己早先弃用的方法，才把这个洞补上。1995 年 5 月，这份 129 页的证明正式发表。

慢还不是最麻烦的地方。托马斯·黑尔斯（Thomas Hales）1998 年证明开普勒猜想，评审花了四年，12 人评审团最后只给出「99% 确定」的结论。他后来带一个 20 人的团队做了 Flyspeck 项目，把这份证明形式化。佩雷尔曼 2002 年的庞加莱猜想证明，数学界用了大约四年才接受，其间发表了三篇各 300 页的阐释文章。赫尔夫戈特 2013 年的弱哥德巴赫猜想证明，到今天还在评审。有些证明后来被发现是错的，却被接受了多年，其他数学家又拿它们当地基继续往上盖。

Anthropic 文章里还有个更小的例子。Tianyi Peng 本科时，导师想把他的论文结果写进一篇 Nature 文章，问他「你确定这个证明是对的吗」。他的回答是：「我 99% 确定，但这么长的证明很难 100% 确定。」那次他的工作没上成 Nature。

问题不在人不够聪明，而在方式：读一份长证明，等于让几个人从头到尾把一本书读完，还要保证每一页都没错。机器验证想换一种方式——不是让人去信一个结论，而是让程序把每一步重跑一遍。

同一份证明，两种检查方式

机器凭什么能检查数学？人写的证明不能直接喂给它吗？

把写给人的证明，翻译成机器要的每一步

所谓形式化，就是把一篇写给人类读的证明，改写成证明助手能逐行核验的语言。Anthropic 用的是 Lean。

人类写的证明天然会跳步。「由前述显然可得」这样的句子，靠的是作者和读者之间的默契；Lean 不认这份默契，它要求每一步推理都显式写出来，从公理出发一个符号一个符号地推到底。中间断掉任何一环，编译就会报错，后面的结论全部作废。

另一半冗长来自积累。人类证明站在几个世纪的已发表工作之上，随手就能引用别人证过的定理；形式化却只能从「已经被形式化过的那一小部分数学」出发，剩下的都要自己补。两头的落差叠起来，就是 1300 万行这个体量的来源——写给人的证明越简洁，翻译成 Lean 就越长。

还有一个尺度容易被误读。Anthropic 自己说，这份证明的规模是 Mathlib 的五倍以上。Mathlib 是 Lean 社区共同维护、由人类精简并反复评审的基础库。五倍说的是体量，不是质量，也不是难度；Anthropic 也承认，这份证明很可能比实际需要的长得多。

上千万行拆给几十个协作者，谁来决定下一步证哪个？

几十个 AI 一起做 11 天，靠一张图纸才没乱

把上千万行拆给几十个 Claude 智能体，遇到的第一个问题是：它们会忘记项目做到哪了。

Claude 的初版尝试就是这样失败的——智能体早期确实取得了一些进展，开始定义概念、证明中间定理，但很快失去对项目状态的跟踪，停止有效协作。这次失败没有白费：它留下的代码约占最终证明非样板代码行的 7%。

转折点是改用 Prove2Me，一个由 Tianyi Peng 和他在哥伦比亚大学的合作者设计的开放协作平台。它做了三件很具体的事。

第一，维护一张定理陈述的有向无环图：每条待证、已证的定理是图上的一个节点，智能体照着图决定下一个该攻哪个。这既缓解了长任务里的记忆退化，也让多个智能体可以并行推进。

第二，把定理陈述和证明拆进不同文件，独立维护两者的链接，Lean 编译因此更快、更省资源。

第三，给每条定理配一句自然语言描述，方便搜索和复用，证明路径因此更简单。

配上基于 Claude Code 的多智能体框架，几十个智能体在 11 天内把根定理一路推到「已证明」。日志里留下了那一刻：「FLT 根节点显示 Proved。历史性时刻（待复查）。」

根节点写着 Proved，就代表这份证明过关了吗？

这份证明过了哪几道关

「Proved」只是平台上的一个状态，真正让它站住的是后面几道独立的检查。

第一道是 Lean 内核：最终证明通过检查，并且只用到 Lean 的三条标准公理——propext、Classical.choice、Quot.sound。换句话说，它没有偷偷加假设，没有留 sorry 之类的占位符，也没有绕开内核。

第二道是陈述对齐：comparator（一个专门核对证明的工具）确认该定理的陈述与 Mathlib 自身的 FLT 陈述一致。不只是结论对得上，连用到的每个常量都相同，整份证明连同 Mathlib 在内核里重放了一遍。它给出的判定是「Your solution is okay!」。这一步回答的是另一个容易混淆的问题：Claude 证明的确实是费马大定理，而不是某个名字差不多的命题。

第三道是独立内核复检，细节写在 Anthropic 的 GitHub 仓库里。在一次从零开始的完整构建中（Lean 4.33.1，Mathlib 从源码编译），这个仓库的 60,475 个模块全部构建通过，每一条声明都由 Lean 内核检查过。另一个独立内核 nanoda 0.4.13 把同一份东西重放了一遍，检查 1,052,234 条声明，零错误。仓库里也没有任何模块偷偷留后门，比如自己加一条假设，或者让检查跳过某一段。换一种说法：两个互不相关的检查器，放行了同一份证明。

检查本身也不便宜：构建用了 5 小时 32 分（96 路并行），comparator 跑了约 15 小时，光是导出的证明环境就有 37.8 GB。

至于产出这份证明的代价，是整个工作消耗约 6,000,000,000 个输出 token（词元，粗略说就是模型写出来的文字量）。这些 token 来自一个未具名的通用内部研究模型，Anthropic 说它大致相当于 Claude Fable 5.1。

检查做得这么细，这份证明就没有可挑剔的地方了吗？

1300 万行里，机器管不了的那部分

Anthropic 自己承认，这份证明的规模是 Mathlib 的五倍以上，而且很可能比实际需要的长得多。原因是两边的目标不同：Mathlib 由人类维护多年，精简，并且经过反复评审；Claude 的证明追求的是被机器接受，不是被人读懂。

定理命名同样如此。名字由流水线自动生成，Anthropic 明确说：名字和陈述冲突时，以陈述为准。

于是留下一条绕不过去的边界。Anthropic 的 GitHub 仓库把它写得比谁都直白——没有工具能检查每个中间定理是否真的意味着它名字所暗示的意思，这件事只能由读者判断。也就是说，机器能确认「从公理到这里，逻辑链成立」，确认不了「这条定理说的是我们以为的那件事」。语义是否符实，仍然要人类数学家逐条核对。

另外两件事也该一起说清。第一，这次形式化沿用的是怀尔斯路线的简化版本，它不产生新数学。第二，11 天、1300 万行、29,500 个定理、60 亿输出 token 这些数字都出自 Anthropic 一方，目前没有第三方复跑过这份证明。

那这份证明真正改变的，是谁来替我们检查？

以后的论文，可能都要附一份机器验过的证明

Anthropic 对这件事的期待，落在数学界以后怎么消化 AI 成果上。

过去，一份新证明要花几个月到几年评审，错误可能长期潜伏；现在，「给论文配一份机器验证过的证明」正在变成可以预期的标准动作。他们不认为形式化证明能替代写给人看的数学阐释，但在 AI 产出越来越多的前提下，这可能是数学界唯一跟得上的办法。在他们看来，形式化也是少数可以明确说「AI 的角色是好的」的方向。

应 Anthropic 邀请审阅这份 Lean 证明后，Kevin Buzzard 给出了两段评价（由 Anthropic 转述）。一段针对这次：「这项非凡的自动形式化成就在 11 天内证明了费马大定理，除了数学公理之外不依赖任何假设……我们还认识到，AI 自动形式化的产物已经足够结实，可以在上面继续盖楼。」另一段说得更远：「如果 FLT 的自动形式化现在就能做到，那我们已经朝着现代数学文献的自动形式化迈出了一大步……这些技术也会让我们能严格检查 LLM（大语言模型）生成的数学——那目前通常是人力成本极高的过程。」

还有一条容易被忽略的线索：写 Lean 也在反过来帮 Claude 做出新结果。Anthropic 说，他们近期不少由 Claude 完成的结果都同步做了形式化。Claude 会用这些部分证明回过头检查自己的假设，就像它写数值模拟来确认方向一样。

门槛也在往下掉。Anthropic 做了个小实验：三个个人版 Claude Max 订阅，让智能体完全通过 Prove2Me 协作，3 天完成了维诺格拉多夫三素数定理的形式化。这个实验没有交代智能体数量、token 消耗，也没说是否经过完整的 Lean 检查，规模更是远小于 FLT。但它的意思很清楚：配上合适的工具和分工方式，消费级订阅也能参与重要定理的形式化。与此同时，Anthropic 和其他实验室都扩大了对外部研究者的支持，包括免费与折扣订阅、研究额度，以及面向大型科学项目的专项资助。

对不研究数学的人来说，这份证明能留下什么？

以后看到「AI 证明了 X」，先问三句话

对不研究数学的人来说，这份证明马上能用上的一点，是判断顺序的变化。

以后再看到「AI 证明了某个结论」，先看有没有形式化文件。只有论文或博客稿时，正确性仍然靠传统人审；有形式化文件并通过内核检查时，逻辑链的正确性已经是机器可确认的事实，剩下的语义判断依然要人来做。

接着看验证的到底是什么：是完整逻辑链，还是只编译通过；用了几条公理，有没有 sorry 之类的占位符；定理陈述有没有和公认版本对齐过。

最后再看命名与陈述。机器管不了名字和实际含义是否对得上，这一层只能由数学家逐条核对——这也正是这份 1300 万行证明最需要人工阅读的部分。

Anthropic 在文章结尾提了一句：数学界现在普遍认为，费马页边那句「奇妙证明」其实是错的，因为三百多年里没人找到过初等证明。机器验证复不活那句话，但它能让数学界不再靠奇迹与信任维持地基。从 1637 年的页边批注，到 1995 年那 129 页，再到这次 11 天里生成的 1300 万行代码，费马大定理的故事多了一段尾声。证明这件事，正在从「说服同行」变成「通过检查」。