Claude 用 11 天形式化费马大定理：真正的分水岭是交付可核验成果
1300 万行代码证明了什么
2026 年 9 月 4 日，Anthropic 公布：研究员彭天翼提供少量高层指导，数十个 Claude 智能体借助协作平台 Prove2Me，用 11 天将费马大定理的一条完整证明路线写成 Lean 4 代码。项目生成约 30,300 个可验证定理，其中约 29,500 个进入最终证明；源码约 1300 万行，消耗约 60 亿个输出 token。
这不是 Claude 重新发现了费马大定理，也不是一条比怀尔斯证明更短的新路线。项目沿用 Frey、Serre、Ribet、Wiles 和 Taylor–Wiles 奠定的理论链条，具体参考 Darmon、Diamond、Taylor 的简化版本，并复用了 Mathlib、帝国理工学院 FLT 项目及 flt-regular 的部分人类成果。Claude 完成的是形式化：把写给数学同行的证明展开为定义、引理、依赖和证明项，使小型程序内核能够逐步验收。
现代证明依赖大量专家默认接受的背景，但 Lean 不接受“显然”“标准结论”或名称相似。每个对象都要先定义，每次推导都要给出前提，最终依赖必须落到明确的公理和类型规则上。因此，这项工作的意义不是“AI 又答对一道名题”，而是通用模型、任务图、共享检索层和确定性验证器首次在数万个相互依赖的节点上交付了硬验收成果。
验收边界也比通常的模型自评严格。最终定理只依赖 Lean 的三个标准公理 propext、Classical.choice 和 Quot.sound；默认构建拒绝 sorry、新增公理和 native_decide 等绕过证明的方式；Comparator 将最终陈述与 Mathlib 中的费马大定理逐项比对；独立 Rust 内核 nanoda 又检查了 1,052,234 个声明，没有报错。公开复现实测并不轻巧：全量构建曾耗时 5 小时 32 分钟、峰值内存 153GB，Comparator 单核重放接近 15 小时、峰值内存 230GB。但外部团队至少不必相信一句“模型说它证明了”，而可以下载产物并运行检查器。
最准确的定义是：这不是费马大定理的第二次发现，而是一次把超长数学工程转化为可执行证据的压力测试。
从同行审查到机器验收
费马在 1637 年写下页边命题。1993 年，Andrew Wiles 宣布完成证明，两个月后审稿发现关键缺口；他又花约一年并与 Richard Taylor 合作修补，最终于 1995 年发表正确证明。这段历史揭示了现代数学的结构性难题：前沿证明依赖少数专家共享的隐性知识，同行审查虽然严格，却昂贵、稀缺且难以扩容。
类似问题推动了形式化证明的发展。Thomas Hales 的开普勒猜想证明经过多年审查，评审团队一度只能表示“99% 确信”；此后 Flyspeck 项目用 HOL Light 和 Isabelle 检查整套证明。四色定理、奇数阶定理和液态张量实验也表明，证明助手能够承载复杂数学，而不仅是教科书习题。
形式系统解决的是信任的最后一公里：自然语言解释“为什么这个想法成立”，证明助手检查“每一步是否真的成立”。两者长期难以结合，主要障碍不是逻辑，而是成本——把几十页论文翻译成数十万乃至数百万行形式语言，本身就是专业而缓慢的劳动。
Lean 与 Mathlib 提供了复利基础
Lean 不只有小型可信内核，也是一门可编程语言；社区可编写自动化策略，并通过 Mathlib 共享定义和定理。拓扑空间、测度、范畴或伽罗瓦表示一旦被形式化，后来者便不必从集合论底层重建。库越厚，可表达的问题越复杂；更复杂的问题又迫使库补齐缺口，形成软件工程式复利。
液态张量实验进一步证明，Lean 可以承载当代研究数学，并能发现自然语言证明中需要补充的条件。形式系统由此成为一种特殊同行：它没有直觉，却不会因作者声望、行文流畅或领域惯例而放过缺失条件。
帝国理工学院的 FLT 项目正沿这条路线推进。Kevin Buzzard 在 2023 年底判断，当时 AI 尚不足以真正帮助这项形式化；项目从 2024 年 10 月进入资助周期，计划持续至 2029 年。它从证明顶端和 Mathlib 基础两端推进，重视自然定义、稳定接口、可读性、复用与长期维护。其目标不只是让最终节点通过，而是建设可继续扩展的公共基础设施。
Claude 的“11 天”因此不能脱离数百年的数学积累、Lean 与 Mathlib 的建设，以及 Imperial FLT 和 flt-regular 的既有成果来理解。真正可复制的技术不是凭空创造全部组件，而是把成熟组件接成新的生产系统。
数学 AI 如何从短题走向长程工程
早期 AI 定理证明主要成长于“短题、闭世界、强反馈”的环境。miniF2F 将 488 道奥数和高校数学题整理成跨证明系统基准；LeanDojo 提供程序化交互、前提检索和近十万个 Mathlib 定理构成的评测集；DeepSeek-Prover-V1.5 把证明助手反馈接入强化学习和蒙特卡洛树搜索，在 miniF2F 与 ProofNet 上分别报告 63.5% 和 25.3%。
Google DeepMind 的 AlphaProof 将语言模型与 AlphaZero 式强化学习结合，在 Lean 中生成并检查证明。它与 AlphaGeometry 2 解决了 2024 年国际数学奥林匹克竞赛六题中的四题，获得 28 分，达到银牌上沿。不过，比赛题仍需人工翻译为形式语言，部分题目需要计算数小时至数天。
这些系统擅长在已定义的命题上搜索证明：目标明确、错误反馈快速、最终结果可判定。费马项目的难点不同。许多对象尚未进入现成库，数万个子定理彼此依赖，没有任何单个智能体能把全局状态长期装在上下文窗口中。问题从“能否解出当前证明状态”变成“如何让几万个局部成果最终汇入同一个根节点”。
决定性变化是把记忆搬出模型
彭天翼团队最初直接让多个 Claude 协作，智能体虽然能解决局部证明，却会忘记工程进度，不知道其他实例完成了什么，也无法稳定复用成果；最终证明中约 7% 的非模板代码来自这些早期尝试。
转折点是 Prove2Me。平台没有追求无限上下文，而是把工程状态外置为有向无环图：顶层是费马大定理，下层是可独立认领的定义和子定理；节点记录形式陈述、自然语言说明、状态和依赖；结果只有通过 Lean，才能成为其他节点的依赖。平台还把定理陈述与证明体拆到不同文件，降低反复编译成本，并保存自然语言说明供后续智能体检索。
系统不要求任何一个 Claude 记住一切，只要求它对当前节点负责。全局记忆由依赖图保存，局部正确性由 Lean 判断，已完成工作由检索层复用。这更像大型开源软件工程，而不是一个天才在白板前独立完成证明。
Anthropic 还报告了一个规模较小但更接近产品化的实验：三份个人 Claude Max 订阅通过 Prove2Me 协作，在三天内完成 Vinogradov 三素数定理相关形式化。它不能证明所有重大数学项目都能廉价复制，却说明这套流程不必依赖实验室专用证明模型。通用模型配合合适支架，也可能承担大量原本需要专家完成的形式化劳动。
真正的节点因此不是“费马大定理终于被计算机证明”，而是形式化劳动的边际成本开始呈现类似软件生成的下降曲线，同时验收标准没有随着生成规模变软。
同期路线解决的不是同一个问题
人类主导的大型形式化项目，如 Imperial FLT、Flyspeck 和 Liquid Tensor，重视可读、可维护、可复用的数学接口，但周期以年计，专家供给稀缺。AlphaProof 和 DeepSeek-Prover 等专用系统面向已经形式化的命题，优势是证明搜索闭环清晰、评测可量化，短板是依赖正确的题目形式化，并不天然擅长超长依赖图。
FunSearch 则由语言模型生成程序，再用自动评估器筛选和迭代，在 cap set 与装箱算法中得到过新结果。它与形式证明共享“开放生成、严格验收”的结构，但评估器通常判断构造有多好，Lean 检查命题能否由给定公理推出。前者允许近似解和连续改进，后者提供二元验收。验证器既扩大了 AI 的可靠工作范围，也限定了赛场：只有可形式化或可计算的目标才能进入闭环；“定义是否自然”“路线解释了什么”“猜想为何值得研究”仍没有类似 Lean 内核的完备裁判。
Claude 与 Imperial FLT 看似参加同一场比赛，目标函数却不同。Anthropic 仓库复用了 Imperial 等来源的 106 个文件，但仓库明确定位为不维护、不接受贡献的研究产物；源码由 AI 生成，注释大多移除，命名可能只是流水线标签，名称与声明冲突时以声明为准。Imperial 项目建设的是可以继续扩展的公共道路，Anthropic 先交付了一条通过结构检验、直达终点的高架桥。
1300 万行既是能力证据，也是债务规模。它超过 Mathlib 体量的五倍，不等于包含五倍的人类数学知识。自动产物可能重复相近结论、采用不自然定义，或用很长路径绕开专家眼中简单的引理。内核能保证逻辑成立，却不能判断抽象是否优雅、模块是否值得复用。
真正改写的是 AI 的交付结构
这次成果最有普遍价值的部分，是“验证与生成分权”。Claude 负责提出证明代码，Lean 内核负责接受或拒绝；Comparator 检查最终证明的是否确为预定命题；nanoda 用第二套内核实现降低单一检查器缺陷的风险。规模扩张发生在不可信的生成侧，信任锚则保留在小型、稳定、可审计的验证侧。
这比让模型生成答案后再自我评价更可靠，也不只适用于数学。代码智能体可以留下单元测试、类型检查、静态分析和可复现构建；数据智能体可以交付 SQL、数据血缘和可重算指标；投研智能体可以留下证据、时间戳与公式供独立程序复算。分水岭不是模型能否写出更像专家的答案，而是产物离开模型后能否继续被检查。
但软件式正确不等于数学式理解。Lean 只能保证实际声明间的推导成立，不能保证定理名称、英文摘要与人类概念一致。Anthropic 仓库也承认，Lean 声明才是权威，源码主要为了被检查，而不是被阅读。逻辑无误却无人愿意维护的 1300 万行仓库，更像证书而非知识库。
下一轮竞争会从“能不能证明”转向压缩率、复用率、接口质量和人类审阅成本。如果 AI 能将这些代码重构到数学家可导航的规模，并把通用部分稳定并入 Mathlib，其影响会远大于再完成几个一次性名题。若每个成果都产生一座耗费数百 GB 资源、几乎无法维护的代码山，瓶颈只会从判断真假转移到理解和治理依赖。
接下来可能发生什么
最可能的变化，是形式化证书成为高价值数学成果的第二交付件。未来三到五年，自然语言论文仍负责概念、动机和路线，Lean、Rocq 或 Isabelle 代码负责逻辑闭合；代数、组合与理论计算机科学等较易形式化的领域可能率先试点。审稿人的工作也会从逐行寻找逻辑漏洞，转向核对命题选择、定义对应与研究价值。
最危险的变化，是“检查器通过”制造新的信任错觉。形式命题可能弱于自然语言主张，定义可能嵌入有争议的选择，现实领域的模型假设也可能脱离数据。纯数学的公理边界相对清晰，金融、医学和物理中的形式证明只能说明结论在给定假设下成立，不能证明假设忠实描述世界。完整重放还需要较高算力和内存，“代码公开”不等于普通研究者可以低成本验证。
最乐观的变化，是机器证书反过来提高 AI 的原创数学能力。大量文献一旦被形式化，模型得到的将不只是训练文本，而是一张包含定义、依赖、反例和失败路径的知识图。模型可以在提出猜想时立即尝试局部形式化，用内核反馈排除错误方向，再把成功结构交给人类解释。生成与验证由此从前后两站变成持续循环。
判断这些剧本走向的指标很具体：第三方能否以合理资源复现公开仓库；自动代码有多少能进入长期维护的公共库；形式陈述与论文主张是否明确映射；人类审阅时间是否真正下降；系统能否在没有既定证明路线时产生新颖且可理解的数学。
结论
费马大定理像一块巨大而严格的试金石。它不仅测试模型能生成多长的推理链，更迫使系统回答：状态放在哪里，依赖如何共享，错误由谁拦截，成果怎样由陌生人重放。
这项成果的行业价值或许高于其数学新闻价值。它给出了长程智能体的一种清晰架构：把记忆放进外部状态，把任务放进依赖图，把局部尝试交给模型，把最终裁决交给独立验证器。模型能力决定单个节点走多快，支架决定节点能否累积，验证器决定累积出来的东西是否值得相信。
1300 万行暂时还不是适合人读的数学作品，更像一张体积惊人的收据：每一笔逻辑支出都可以对账，代价是冗长、昂贵和难以维护。下一步不是打印更长的收据，而是在保留可靠性的同时，让成果更短、更清楚、更适合继续建设。
费马曾说页边太窄，写不下那个“绝妙证明”。三百多年后，AI 走向另一个极端：它用了 1300 万行，让机器确信每一步都已写下。下一道题不是还能写多少，而是人和机器能否共同理解哪些行真正重要。
事实限定与风险边界
- “首个完整、机器检查的费马大定理证明”是 Anthropic 对该项目的表述，虽有公开代码、Kevin Buzzard 审阅、Lean 构建、Comparator 和 nanoda 检查支撑，但不等同于已经完成传统期刊同行评审。
- 项目形式化的是既有证明路线，不是费马大定理的新证明，也没有解决黎曼猜想或 Navier–Stokes 等未解问题。
- “11 天”仅指集中运行周期，不包括数百年的数学积累、Lean 与 Mathlib 建设、Imperial FLT、
flt-regular及 Prove2Me 的研发时间。 - 60 亿输出 token、11 天和 30,300 个定理等过程数据主要来自 Anthropic。公开仓库可核验最终产物，但不能单独重建全部生成过程与人工干预记录。
- Lean 验证的是形式陈述能否从给定公理推出，不自动保证命名、自然语言解释、概念选择、数学价值或现实假设。
- 完整第三方重放需要较高内存、磁盘和计算资源；公开可检查不代表个人可以低成本完成全量验证。
信息来源
访问日期均为 2026 年 9 月 6 日。
- Anthropic：Formalizing Fermat’s Last Theorem，2026-09-04。
- Anthropic：Fermat’s Last Theorem in Lean 4（GitHub）。
- Shuze Chen 等：Prove2Me: An Open Collaborative Platform for Scaling Math Formalization，arXiv:2608.28433，2026。
- Imperial College London：Fermat’s Last Theorem Formalisation Project。
- Kevin Buzzard：A Lean formalisation of Fermat’s Last Theorem: General Information。
- Henri Darmon、Fred Diamond、Richard Taylor：Fermat’s Last Theorem。
- Google DeepMind：AI achieves silver-medal standard solving International Mathematical Olympiad problems，2024-07-25。
- Google DeepMind：FunSearch: Making new discoveries in mathematical sciences using Large Language Models，2023-12-14。
- Kaiyu Yang 等：LeanDojo: Theorem Proving with Retrieval-Augmented Language Models，NeurIPS 2023。
- Huajian Xin 等：DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search，2024。
- Kunhao Zheng、Jesse Michael Han、Stanislas Polu：MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics，ICLR 2022。
- Peter Scholze、Dustin Clausen、Johan Commelin、Patrick Massot：Blueprint for the Liquid Tensor Experiment。
- Thomas Hales 等：A Formal Proof of the Kepler Conjecture，*Forum of Mathematics, Pi*，2017。
- 智东西：刚刚，Claude 11天验完费马大定理！清华姚班大牛带队，用AI拿下大结果，2026-09-05。