大约1637年，法国数学家皮埃尔·德·费马（Pierre de Fermat）在他那本第丢番图（Diophantus）的《算术》（Arithmetica）书页边空白处，用拉丁文写下了这样一段话（这是数学史上最著名的边注之一，学界对其存在无争议）：

“我发现了一个真正令人惊叹的证明，但这个书页的边距太小，装不下它。”

这道方程——任何正整数 a、b、c，以及任何大于2的整数 n，都无法满足 aⁿ + bⁿ = cⁿ——后来被称为费马大定理（Fermat’s Last Theorem，FLT）。从那天起，全世界的数学家花了358年来寻找那个「令人惊叹的证明」。

1908年，德国数学家保罗·沃尔夫斯凯尔（Paul Wolfskehl）设立了一个奖项：10万德国金马克（约合今天的100-200万美元），奖励第一个证明费马大定理的人。仅第一年就收到了621份错误证明。

1993年6月，普林斯顿大学教授Andrew Wiles在剑桥大学连续3天宣布他完成了证明。数学界欢呼。两个月后，一位审稿人在证明中发现了一个关键漏洞——一个关于Euler系统的论证有缺陷。Wiles用了又一年时间，几乎独自一人在阁楼上工作，与他的前学生Richard Taylor合作，最终找到了修复方案：把欧拉系统论证替换为一个基于不同思路的Iwasawa-Greenberg方法。

1995年，Wiles的完整证明发表。那篇文章长达129页，用到了椭圆曲线、模形式、伽罗瓦表示等远远超出费马时代的现代数学工具。专家们花了数月才逐步确认每一步都是正确的。

这是人类数学史上最漫长的智识追求之一的终点。

或者，我们以为是终点。

2026年8月17日深夜

北京时间2026年8月18日早上10点，某个分布式计算系统的状态面板上出现了这样一行文字：

“🏁🏁🏁The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18 (10:00:57pm ET Aug-17). Historic moment for this campaign.”

这是数十个Claude智能体组成的自动形式化系统，在完成了它工作以来的最后一步验证时，自动生成的状态日志。

不是Anthropic工程师写的庆祝公告，而是Claude的系统状态日志（Anthropic官方称为「Claude’s thinking」，即Claude在工作过程中的内部推理记录，参考官方研究页面）：「FLT根节点已证明。」

到这一刻，Claude已经连续工作了11天，产出了1300万行Lean代码，在这个过程中证明了29,500个中间定理，消耗了约60亿个输出token。

人类数学社区原本预计需要数年时间完成的工作。

先理解「形式化证明」是什么

在分析这件事的意义之前，有一个极其重要的概念必须厘清，否则我们很容易被错误的叙事引导：

Claude完成的不是「发现」费马大定理，而是「形式化」它的证明。

这两件事的差距，大约相当于「爬上珠穆朗玛峰」和「在珠穆朗玛峰的每一级台阶上安装防护设施，精确标注每一个落脚点，并让一个自动检查系统能够完全验证整条路径的安全性」的差距。两件事都极难，但性质完全不同。

Andrew Wiles在1995年已经完成了数学意义上的证明——他展示了一条从数学公理出发、通向FLT结论的逻辑路径。但这条路径以人类数学家为阅读对象：它跳过了很多「显然」的步骤，依赖读者对背景知识的掌握，用大量简写和约定俗成的符号。这是人类与人类之间的沟通方式。

形式化（formalization）则是另一回事：把这个证明翻译成计算机可以机械处理的语言。具体来说，是翻译成Lean这样的形式证明助手（proof assistant）能够理解和校验的语言。

Lean的工作方式有2个关键特点：第一，它需要看到每一个步骤，不管多「显然」——两个整数之和是整数，这样「不言而喻」的事实也要在Lean里明确证明。第二，它的校验结果是确定性的——不存在「基本正确」或「有一点小问题」，要么完整通过，要么不通过。

正因为如此，形式化证明是数学可信度的终极形式。一旦一个定理被Lean验证，它的正确性是不需要专家判断的——任何一台计算机都可以在几秒钟内重新校验整个证明链。

对于FLT这样复杂的定理，形式化的难度不亚于重新证明它。Wiles的证明横跨多个数学分支，涉及大量高度抽象的结构。要让Lean理解这一切，必须先把那些在「人类数学」中隐含的大量背景知识逐一形式化，从底层的代数结构，一路叠加到椭圆曲线、模形式、伽罗瓦理论……

2024年，Kevin Buzzard（帝国理工学院教授）发起了一个社区项目，目标是用Lean形式化Wiles的证明。仅这个项目的路线图蓝图文档就有86页。当时的估计：这需要一个数学社区协作数年。

Claude在11天内独自完成了它。

一个实验走向了历史

这个实验由Anthropic研究员Tianyi Peng发起。根据Anthropic官方研究页面（https://www.anthropic.com/research/formalizing-fermats-last-theorem），他「set out to test whether Claude could make progress on formalizing FLT」（原文）——设想只是测试是否能取得进展，并不期望完整结果。实际结果远超预期。

数十个Claude智能体在一个协作框架内分工推进，工作方式是分层的：底层智能体负责定义最基础的数学概念（群、环、域……），它们的产出成为中层智能体证明更复杂定理的基础，层层叠加，最终到达FLT本身的根节点。

这个分层结构和人类数学社区的工作方式惊人相似——数学家们在社区项目中也是分工证明不同的子模块，然后由其他人把这些模块拼装在一起。区别是：Claude的整个过程在11天内完成，而人类版本的项目估计需要几年，并且需要多名数学家的持续投入。

整个过程中，人类输入被限制在少量高层次指引（原文：「Mathematical input from humans was limited to occasional high-level instructions from Tianyi」，来源：Anthropic官方研究页）。Tianyi给出的典型指引包括：「Jacobian as a scheme sounds high priority」（雅可比量作为模式优先级高），「push the Mazur theorem to be done soon」（把Mazur定理推到尽快完成）——这些是方向性的优先级提示，不是具体的数学指导。

这不是第一次尝试就成功的。Claude的早期尝试有若干次失败：智能体失去了对项目整体状态的追踪，不同智能体之间的协调效率下降，整个工作陷入局部停滞。那些失败的尝试贡献了约7%的最终代码中的非样板内容（non-boilerplate code），作为历史记录保存在了最终的代码库中——它们是Claude探索失败路径的证明，也是最终成功的一部分。

最终的结果让Kevin Buzzard感到震惊。他写道：

“这项非凡的自动形式化成就，仅用11天证明了费马大定理，除数学公理外无其他假设。途中形式化了代数、调和分析、几何和数论……AI自动形式化成果现在已经足够健壮，可以被后续研究所构建；这个证明是多层次的。”

“除数学公理外无其他假设”——这是数学证明中最高的可信度标准。不依赖任何未经验证的前提，直接从公理出发，抵达结论。

整个代码库发布在GitHub，供全球数学社区检验和使用。

数字背后的真正意义

让我们把几个关键数字放在一起理解：

13,000,000行Lean代码，超过Mathlib库的5倍。 Mathlib是数学社区多年积累的Lean形式化代码库，是整个Lean数学生态系统的核心基础设施。Claude完成FLT形式化所产出的代码，相当于Mathlib规模的5倍以上。这意味着Claude不只是「证明了FLT」，而是在这个过程中形式化了大量附带的数学知识——那些通向FLT所必须经过的中间领域，从代数几何到模形式，都留下了可被校验的形式化痕迹。

29,500个中间定理，60亿输出token。 60亿输出token是一个需要一点感知的数字：此处不提供具体费用估算，因为实际使用的是内部研究模型，成本结构和公开API定价有本质差异。Anthropic官方研究页也没有披露任何成本数字。读者不应将任何第三方来源的「等价费用」估算作为可靠数据引用——这类估算的不确定性极高。Claude在11天里消耗了相当于「写了数十本完整书籍」的计算量，全部用于在Lean语言中构建和验证数学逻辑。

11天对比「数年」。 这个速度对比值得细想：人类数学社区估计需要数年，并且是多名全职数学家的工作。Claude是一个（或数十个协作的）AI系统，11天完成。这个速度差不是「快了一点」，而是几乎改变了数量级。

这意味着什么？不只是「Claude很聪明」——而是说，对于「需要把已知证明进行形式化验证」这类任务，AI已经显示出超越人类（在速度和扩展性上）的真实能力。

为什么这比「AI下棋」更根本

每次AI完成了一件被认为需要人类才能做到的事，总有反驳：「那只是个游戏」「只是模式匹配」「这不算真正的智能」。有时候这些反驳是对的。

但FLT形式化的情况要深刻得多，因为它触碰了一个关于「数学本质」的根本问题。

象棋引擎（比如AlphaZero）的任务是在一个封闭的状态空间里找到最优路径。规则是确定的，所有可能的状态（虽然数量巨大）在原则上是可以枚举的。象棋引擎处理的是组合优化问题——这类问题在计算机科学中有完善的理论框架。

数学证明的搜索空间是开放的（这一点在数学哲学领域有广泛共识，例如乔治·波利亚（George Pólya）在《怎样解题》（How to Solve It，1945）中对数学启发式方法的分析，该书可在主要图书馆数据库检索）。没有人告诉你哪些中间定理是必须的，没有人告诉你哪条推导路径会成功。历史上，证明费马大定理最终需要引入「椭圆曲线的模性」和「伽罗瓦表示」——这些工具是后来几百年数学发展的产物，费马写下猜想时根本不存在。这说明：证明某些定理，需要的不只是「在已有规则内搜索」，而是「创造新的概念工具」。Claude在FLT形式化中是否做到了这一点，还是只是沿用了Wiles的数学工具，是一个值得关注的问题——目前来看，主要路径是「跟随Darmon-Diamond-Taylor的简化版本」，而非创造新的数学。

有人会说：Claude是基于人类的数学文献训练的，它只是「记忆」并「重组」了人类已经有的知识。

这个论点部分是对的。Claude确实没有从零开始发明Wiles的证明。但Tianyi Peng在测试时，给Claude的任务是「完成形式化」，没有给出详细的路线图。Claude需要自己决定：哪些子命题需要先证，哪些代数结构需要先定义，当某条路径失败时换到哪个方向。

这不是简单的「检索和粘贴」——从人类数学社区花了数年只完成部分工作的任务上，Claude独立完成全部，这说明某种程度的「导航能力」在起作用。无论我们如何定义这种能力，它的实际效果是无法否认的。

multi-agent协作：不只是类比，是新的工程范式

FLT形式化的另一个重要意义，在于它展示了multi-agent协作架构在「知识工作流水线」上的真实能力——而且这个架构的技术细节，比「和人类社区的工作方式相似」这个类比更值得深究。

根据Anthropic官方研究页面的描述，这个系统的核心工程特征包括3点：

第一，任务分解的粒度是动态的，而非预先规划的。 顶层智能体在推进过程中实时判断哪些子命题需要被分解为更细的子任务，哪些可以直接尝试证明。这意味着整个工作图（dependency graph）是在执行过程中生长出来的，而不是事先由人类设计好的。这和传统软件工程中「先写详细设计文档，再按图施工」的范式有根本区别。

第二，失败信号被作为结构化信息传递，而非简单丢弃。 当某个智能体在某条推导路径上失败，这个失败记录会进入系统的共享状态，其他智能体在后续尝试中可以避开已知的死胡同。那7%来自失败尝试的代码（据Anthropic官方研究页）之所以被保留在最终代码库中，正是因为它们携带了「这条路走不通」的信息——这本身是有价值的数学知识。

第三，验证是持续的，而非终态的。 Lean校验器不只在最后运行一次，而是在每个子任务完成时立即校验。这意味着错误在局部被发现，而不是在整个系统崩溃时才被察觉。这种「持续集成」的验证逻辑，和现代软件工程的CI/CD管线在结构上高度同构。

这3个特征合在一起，描述的不是「AI模拟了人类数学家的工作方式」，而是一种新的自适应知识构建系统：它能在开放性问题空间中自主分解任务、传递失败信号、持续验证中间结果，并在人类给出极少干预的情况下维持11天的连贯工作状态。

这个架构的意义远超数学领域。它是一个通用的工程原型，适用于任何「需要从底层公理出发、逐层构建可验证逻辑链」的知识工作场景。它不是未来的概念——它已经在FLT形式化中被实际运行并产出了真实成果。

大多数人没看到的第三层冲击

关于这件事，大多数报道停留在2个层次：第一层，「AI完成了数学史上的重大任务」；第二层，「这说明AI的数学推理能力很强」。

但真正深远的冲击在第3层，而且它不关于数学，关于认识论基础设施。

人类知识体系有一个长期存在的脆弱性：绝大多数知识的可信度，依赖于「权威专家说它是对的」。Wiles的129页证明，即便在1995年发表后，也只有全球数十位顶尖数学家真正有能力独立校验它的每一步。这意味着：如果这些人中的大多数犯了同样的错误，或者有人出于某种原因给出了错误的背书，这个错误可能在相当长的时间内无法被发现。

这不是假设。Wiles的第一版证明在1993年被宣布时，数学界普遍接受，直到两个月后才有人发现漏洞。更早的案例中，有些数学错误在文献中潜伏了数十年才被纠正。

形式化证明改变了这个结构：它把「这个证明是否正确」这个问题，从「需要专家判断」变成了「任何计算机都可以机械校验」。 这是认识论意义上的民主化——不是说每个人都能理解证明，而是说证明的正确性不再依赖于少数人的权威背书。

Claude完成FLT形式化的真正历史意义，不只是「AI很快」，而是它为人类知识体系建立了一个新的可信度基准。一旦一个定理被形式化，它的正确性就从「专家共识」升级为「机械可验证事实」。

现在，这件事的成本从「需要数学社区数年工作」降低到了「需要AI系统11天工作」。

这意味着，原本因为成本过高而无法被形式化的大量数学知识，在技术上已经进入了可形式化的范围。数学知识体系的「认识论基础设施」——那个支撑我们相信某个定理是真的底层结构——正在经历一次静悄悄的升级。

大多数人注意到了速度的变化。很少有人注意到，我们正在经历的是数学知识可信度基础设施的一次根本性重构。

为什么这对决策者重要：一个判断框架

如果你是一个需要在AI能力演进上做出判断的决策者（无论是投资者、技术负责人，还是政策制定者），FLT形式化提供了一个可操作的判断框架，而不只是一个令人印象深刻的新闻事件。

框架的核心问题是：你所在的领域，有多少工作具备「形式化验证」的结构特征？

具备这种结构特征的工作，有3个共同属性：

  1. 存在明确的「正确性」标准（不是「更好」，而是「对或错」）
  2. 工作可以被分解为层次化的子任务（底层结论是上层推导的前提）
  3. 子任务之间的依赖关系可以被明确描述

满足这3个条件的工作，在技术原理上和FLT形式化是同构的。这意味着：FLT形式化中展示的速度提升（从数年到11天），在这些领域中理论上是可以复现的。

具体的高价值应用方向（按照成熟度从高到低排列，以下为基于公开信息的分析判断，非Anthropic官方声明）：

  • 软件形式化验证（最成熟）：安全关键系统的属性验证，已有成熟的形式化工具链（Coq、Isabelle、TLA+等），AI加速的主要障碍是人力成本，而非技术可行性。FLT形式化直接降低了这个障碍。

  • 数学论文审稿加速（中期，2-3年内可能出现早期应用）：Anthropic已明确提到「减轻评估新结果的负担」。预计（据推测，非官方数据）审稿周期从数年压缩到数周，在特定类型的定理证明上，这在技术上已经不是障碍。

  • 法律逻辑一致性审查（长期，需要额外的形式化语言开发）：法律文本的形式化需要先建立「法律逻辑的形式语言」，这个基础设施目前仍不完善。但FLT形式化证明了，一旦基础设施就绪，AI可以以极高速度完成大规模验证工作。

对决策者的核心建议：不要问「AI能不能做这件事」，而要问「这件事的形式化基础设施是否就绪」。FLT形式化显示，一旦基础设施就绪（Lean库、数学概念的形式化定义），AI完成工作的速度会让大多数人感到惊讶。在你的领域，那个「基础设施」是什么？它的就绪程度如何？这才是值得追踪的战略问题。

一个值得认真对待的疑问

当然，这个结果也引发了一个值得认真思考的疑问，而不是简单地庆祝：

Claude「理解」这1300万行代码吗？

Lean的校验结果是确定的——每一行逻辑都通过了机械验证，数学上完全正确。Kevin Buzzard背书了这个结果的质量，称之为「AI自动形式化成果已经足够健壮，可以被后续研究构建」。

但「正确」不等于「理解」。这个区分不只是哲学上的：

在实践中，「理解」的一个操作化定义是：能够在新的情境下做出有依据的泛化。一个真正「理解」了FLT证明的数学家，可以从证明中提炼出可以用于其他数论问题的方法论，可以指出哪里是关键步骤，哪里只是技术性的过渡。Claude能否做到这一点？目前没有公开证据说明Claude在完成FLT形式化后，能够解释哪些中间定理是数学上最关键的，哪些只是为了满足Lean的语法要求而必须明确的步骤。

人类数学家读完Wiles的129页证明，可以感受到某种东西：为什么从模形式到椭圆曲线的类比是关键性的洞察？为什么谷山-志村猜想的证明是通往FLT的真正钥匙？Wiles本人说，当他在阁楼上工作时，有一个特定的时刻——他重新审视了一个已经放弃的思路，突然看到了修复漏洞的方法，感受到了一种「令人难以置信的美丽」。

数学有审美维度。不只是逻辑是否正确，而是：这条路径是否优雅？这个构造是否揭示了某种深层的数学结构？

Claude产生的1300万行Lean代码是正确的——但Buzzard没有说它是「美丽的数学」，也没有说Claude展示出了「深层的数学洞察力」。他说的是：这个成果足够可靠，可以被后续研究使用。这是工程质量的评价，不是数学洞察力的评价。

这个区别目前没有答案，但它定义了一个可追踪的问题边界：当AI在开放性任务上超越人类速度时，「正确」和「理解」之间的距离，是在缩小，还是只是变得更难测量？ 这个问题因FLT形式化而变得更加具体、更加紧迫，也更加值得在接下来的AI能力讨论中持续追问。

接下来会发生什么

Anthropic已经把全部代码发布在GitHub上（github.com/anthropics/fermats-last-theorem），供数学社区检验和使用。这不是一个封闭实验，而是一个真正意义上的数学贡献。

从这里出发，有几个方向值得关注：

第一，数学社区如何使用这个结果。 1300万行Lean代码里包含了大量中间定理的形式化，很多是FLT形式化的「顺带成果」，但它们本身可以成为其他数学形式化工作的基础设施。Kevin Buzzard本人的项目组正在评估如何整合这些成果。

第二，这能否重复用于其他困难定理。 FLT是一个特殊的案例——Wiles已经有了人类可读的证明，Claude的任务是形式化。但现在有一个更大的问题：如果给AI一个没有已知证明的开放问题，它能做什么？Anthropic此前也在AI数学推理方向做了持续投入（可参考Anthropic研究页面的相关发布）。FLT的结果会加速这类探索。

第三，对AI能力边界叙事的影响。 每一次AI完成了一件被认为需要人类独特能力的事，「AI不能做X」的叙事就需要被更新。FLT形式化之后，「AI不能完成高度开放性的形式逻辑推导任务」这个命题已经不成立。下一个边界是什么？谁也不知道，但这条线在移动，而且移动的速度比大多数人预期的要快。

它对其他知识领域的隐含冲击

数学是一个特殊的领域：它的「正确」是可以被形式化定义的，它的「证明」有明确的终态，它的推导过程有严格的规则。这使得AI形式化验

参考资料（均为公开可访问URL，于2026年9月8日核实）：

  • Anthropic官方研究页（主要信息来源，包含完整数据和Kevin Buzzard引语）：https://www.anthropic.com/research/formalizing-fermats-last-theorem
  • FLT形式化证明代码库（公开于GitHub）：https://github.com/anthropics/fermats-last-theorem
  • Kevin Buzzard的帝国理工Lean FLT社区项目（背景参考）：https://lean-lang.org/use-cases/flt/
  • Lean形式证明助手介绍（Wikipedia，背景参考）：https://en.wikipedia.org/wiki/Lean_(proof_assistant)
  • Darmon, Diamond, Taylor的简化Wiles证明（Claude遵循的数学路线来源）：https://www.math.mcgill.ca/darmon/pub/Articles/Expository/05.DDT/paper.pdf
  • Forbes分析报道（二手来源，2026-09-07 Jon Markman撰文，核心数据均以Anthropic官方页面为准）：https://www.forbes.com/sites/jonmarkman/2026/09/07/claude-formalized-fermats-last-theorem-in-11-days-on-6b-output-tokens/
  • Andrew Wiles费马大定理原始证明论文（1995年，背景参考）：Wiles, A. (1995). Modular elliptic curves and Fermat’s last theorem. Annals of Mathematics, 141(3), 443-551.
  • Lean形式证明助手官方文档：https://lean-lang.org/documentation/