跳转至

形式化验证费马大定理：Claude历时11天实现数学史里程碑

文章背景与核心概要

近期，Anthropic 宣布完成了对费马大定理（FLT）的首个完整、经计算机检验的形式化证明。在历时11天的自主运行中，AI 模型 Claude 借助 Lean 编程语言和协作平台 Prove2Me，对该定理进行了端到端的形式化验证。在此期间，Claude 编写了 1300 万行 Lean 代码，并基于标准数学公理证明了 29,500 个中间定理。

这一里程碑标志着人工智能自动形式化（Autoformalization）技术的巨大飞跃，预示着未来自动化工具将极大减轻同行评议的负担，并能够安全地验证复杂的数学文献。本文详细梳理了该项目的背景、技术挑战、Prove2Me 平台的作用以及对未来数学研究的深远影响。

📌 Summary

Anthropic has announced the first complete, computer-checked proof of Fermat’s Last Theorem (FLT). Operating largely autonomously over 11 days, Claude utilized the Lean programming language and the collaborative platform Prove2Me to produce an end-to-end formal verification of the theorem.

Along the way, Claude wrote 13 million lines of Lean code and proved 29,500 intermediate theorems based on standard mathematical axioms. This milestone highlights a massive leap forward for AI autoformalization, suggesting a future where automated tools can significantly lighten the burden of peer review and safely verify complex mathematical literature.

🖼️ Article Hero Image

Formalizing Fermat's Last Theorem

大约在 1637 年，皮埃尔·德·费马（Pierre de Fermat）在他的一本丢番图《算术》的空白处写下了一条断言，后来它成为了数学史上最著名的猜想之一：对于任何 \(n > 2\)，不存在正整数 \(a, b, c\) 满足 \(a^n + b^n = c^n\)。费马大定理（FLT）极其难以证明，安德鲁·怀尔斯爵士（Sir Andrew Wiles）直到 1995 年才发表了第一份长达 129 页的经验证证明。

Around 1637, Pierre de Fermat jotted down a claim in the margin of his copy of Diophantus’s Arithmetica that would become one of the most famous mathematical conjectures of all time: no positive integers \(a, b, c\) satisfy \(a^n + b^n = c^n\) for any \(n > 2\). Fermat’s Last Theorem (FLT) turned out to be incredibly difficult to prove, with Sir Andrew Wiles publishing the first verified proof in 1995, spanning 129 pages.

十年后，荷兰计算机科学家扬·贝尔格斯特拉（Jan Bergstra）提出对怀尔斯的证明进行“形式化”。自那时起，数学家们开始建立各种方法，使用诸如 Lean 等定理证明辅助工具来编码复杂的证明。最近，Anthropic 的研究员彭天一（Tianyi Peng）测试了 Claude 是否能够在 FLT 上取得进展。在 11 天内，Claude 产出了首个端到端的、经计算机检验的 FLT 证明，编写了 1300 万行 Lean 代码，并证明了 29,500 个中间定理。

A decade later, Dutch computer scientist Jan Bergstra proposed "formalizing" Wiles’s proof. Since then, mathematicians have built methods to encode complex proofs using proof assistants like Lean. Recently, Anthropic researcher Tianyi Peng tested whether Claude could make progress on FLT. In 11 days, Claude produced the first end-to-end, computer-checked proof of FLT, writing 13 million lines of Lean and proving 29,500 intermediate theorems.

著名数学家凯文·布扎德（Kevin Buzzard）指出：

这一非凡的自动形式化成就——Anthropic 研究人员称其仅用了 11 天——在不假设除数学公理之外的任何前提下证明了费马大定理。在此过程中，我们看到了代数、调和分析、几何和数论的自动形式化，并且我们了解到，AI 自动形式化产物现在已经足够稳健，可以在其之上继续构建；该证明是多层次的。

Prominent mathematician Kevin Buzzard noted:

This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered.

验证数学证明的挑战

与近期关于黎曼猜想的 AI 驱动工作（产出了新的数学知识）不同，这里的突破在于验证。证明定理需要严密的逻辑链条；如果任何一个环节断裂，其后的一切都可能崩溃。理解一个新的数学成果可能需要数月甚至数年。

Unlike recent AI-driven work on the Riemann hypothesis (which produced novel mathematics), the breakthrough here is the verification. Proving theorems requires rigorous logical chains; if a single link breaks, everything following it can collapse. Understanding a novel mathematical result can take months or years.

费马著名的边白批注声称：

我对此发现了一个真正美妙的证明，但这里的空白处太小，写不下。

Fermat's famous marginal note claimed:

I have discovered a truly marvelous proof of this, which this margin is too narrow to contain.

尽管经过了几个世纪的搜寻和无数次不成功的尝试（包括在 1908 年设立奖金后的单年度内就出现了 621 次错误尝试），人们从未找到过一个初等证明。数学界现在认为费马最初的证明是有缺陷的。

Despite centuries of searching and numerous incorrect attempts (including 621 in a single year after a 1908 prize was announced), no elementary proof has ever been found. The mathematical community now believes Fermat's original proof was incorrect.

形式化费马大定理

诸类 Lean 的证明辅助工具通过算法来验证逻辑，但其难点在于将跳过“显而易见”步骤的人类可读证明，转化为细颗粒度的代码。形式化 FLT 的初始蓝图长达 86 页。

Proof assistants like Lean verify logic algorithmically, but the challenge lies in translating human-readable proofs—which skip "obvious" steps—into granular code. The initial blueprint for formalizing FLT runs to 86 pages.

Claude 通过让数十个 AI 代理（agents）协作来完成这项任务：定义概念、证明中间里程碑，并使用达尔蒙、戴蒙德和泰勒给出的怀尔斯证明简化版本来攻克更难的陈述。

Claude completed the task by letting dozens of AI agents collaborate to define concepts, prove intermediate milestones, and tackle harder statements using a simplified version of Wiles’s proof from Darmon, Diamond and Taylor.

Time progression of FLT formalization

在切换到 Prove2Me 后，这项工作最终取得成功。Prove2Me 是由彭天一及其哥伦比亚大学的合作者设计的一个开放式协作平台。Prove2Me 的辅助作用体现在： 1. 维护定理陈述的有向无环图（DAG），以引导代理下一步证明什么并减轻记忆衰退。 2. 通过将陈述和证明分离到不同的文件中来加速 Lean 编译。 3. 通过对定理陈述进行自然语言描述，实现搜索和重用。

The effort finally succeeded after switching to Prove2Me, an open collaborative platform designed by Tianyi Peng and his collaborators at Columbia University. Prove2Me assisted by: 1. Maintaining a directed acyclic graph (DAG) of theorem statements to guide agents on what to prove next and mitigate memory degradation. 2. Speeding up Lean compilation by separating statements and proofs into different files. 3. Enabling search and reuse via natural-language descriptions of theorem statements.

DAG showing Claude formalizing sub-theorems on the way to FLT
Key milestones from the Prove2Me plan that Claude used to formalize Fermat’s Last Theorem. The three colored sections correspond to three core sub-theorems that Claude had to prove on the way to its final goal. This graph closely follows Wiles’s original proof.

“THE FLT root reads Proved on the site. Historic moment (modulo re-check).”

“!!! The FLT ROOT 62eb32c0 reads PROVED. R = T closed and cascaded to the root. This is the campaign's goal: e2e FLT on prove2me.”

“🏁🏁🏁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 意识到自己刚刚完成了什么时的思考摘录。

Excerpts of Claude’s thinking as it realizes what it has just accomplished.

减轻形式化验证的负担

这一证明的速度证明了对庞大数学领域进行形式化现在是切实可行的。凯文·布扎德指出，此类技术将根除现有数学文献中的错误，减轻审稿人的负担，并严格检验大模型生成的数学内容。

The speed of this proof proves that formalizing large fields of mathematics is now viable. Kevin Buzzard noted that such techniques will root out errors in current mathematical corpora, ease the load of referees, and rigorously check LLM-generated mathematics.

此外，编写 Lean 代码有助于 Claude 在处理新成果时验证自身的推理。在另一项实验中，消费级 Claude 代理仅用了三天时间就将维诺格拉多夫三素数定理进行了形式化。Anthropic 和其他实验室将继续通过免费额度、资助和扩展工具访问权限来支持数学研究人员。

Furthermore, writing Lean code helps Claude verify its own reasoning while working on novel results. In a separate experiment, consumer-tier Claude agents formalized Vinogradov’s Three Primes Theorem in just three days. Anthropic and other labs are continuing to support mathematical researchers with free credits, grants, and expanded tool access.

致谢

这一形式化工作建立在安德鲁·怀尔斯（Andrew Wiles）、理查德·泰勒（Richard Taylor）、格哈德·弗雷（Gerhard Frey）、让-皮埃尔·塞尔（Jean-Pierre Serre）、肯·里贝特（Ken Ribet）、巴里·马祖尔（Barry Mazur）、罗伯特·兰兰兹（Robert Langlands）、杰罗尔德·塔内尔（Jerrold Tunnell）、谷山丰（Yutaka Taniyama）、志村五郎（Goro Shimura）和安德烈·韦伊（André Weil）等人数个世纪数学突破的基础之上。

This formalization builds on centuries of mathematical breakthroughs by Andrew Wiles, Richard Taylor, Gerhard Frey, Jean-Pierre Serre, Ken Ribet, Barry Mazur, Robert Langlands, Jerrold Tunnell, Yutaka Taniyama, Goro Shimura, and André Weil.

该项目整合了伦敦帝国理工学院 FLT 项目、flt-regular 项目的工作，并吸收了更广泛的 Lean 和 Mathlib 社区的贡献。

The project integrated work from the Imperial College London FLT project, the flt-regular project, and contributions from the broader Lean and Mathlib community.

了解更多与资源

完整的证明和书面演练可在 GitHub 上获取。

The full proof and a written walk-through are available on GitHub.

推荐拓展阅读

脚注

  1. 在本科学习期间，彭天一的导师曾问他是否 100% 确信其毕业论文的证明是正确的。彭回答“有 99% 的把握”，却因无法在数学上保证庞大证明的每一个步骤而错失在《自然》杂志上发表的机会。
  2. 其他历史上的验证瓶颈包括托马斯·黑尔斯（Thomas Hales）对开普勒猜想的证明（催生了 Flyspeck 项目）、格里高利·佩雷尔曼（Grigori Perelman）对庞加莱猜想的证明，以及哈拉尔德·赫尔夫戈特（Harald Helfgott）对弱哥德巴赫猜想的证明。
  3. 部分原因是 Mathlib 简洁且经过充分审查，而 AI 生成的证明比严格需要的更长。

Footnotes

  1. During his undergraduate studies, Peng’s advisor asked if he was 100% certain his thesis proof was correct. Peng answered "99% sure," missing out on publication in Nature because he couldn't mathematically guarantee every step of a massive proof.
  2. Other historical verification bottlenecks include Thomas Hales’s proof of the Kepler conjecture (led to the Flyspeck project), Grigori Perelman’s proof of the Poincaré conjecture, and Harald Helfgott’s proof of the weak Goldbach conjecture.
  3. This is partly because Mathlib is concise and well-reviewed, while the AI-generated proof is longer than strictly necessary.