Anthropic称Claude完成费马证明形式化

Anthropic在9月4日披露的核心，是一个可下载、可构建、可由证明助手检查的Lean工程；它不代表AI重新发现了费马大定理。Claude用11天把Wiles和Taylor-Wiles路线转写成端到端形式化证明，并把仓库公开给外部复核。

证据链先落在公开工件上。Anthropic研究页标注发布日期为2026年9月4日，并称这是first complete computer-checked proof of Fermat’s Last Theorem；官方数字写到1300万行Lean、30300个过程中产出的可验证定理、29500个最终使用的中间定理和约60亿输出token。GitHub README则给出验证路径：FinalCheck.lean检查最终定理只依赖Lean的三个标准公理，仓库还提供comparator和nanoda复核脚本。

这套工件仍有现实门槛。Anthropic是本次主要事实源，完整复跑需要很高的机器资源；README写到从零构建需要大量磁盘、内存和时间，comparator单核重放也接近半天以上。因此，本文把“公开了可核验工件”和“全球数学社区已经完成长期独立审查”分开表述。Prove2Me论文和Imperial College London的FLT项目都是关键背景，9月4日的新发布主体是Anthropic证明工件。

这会直接改变AI数学新闻的判断标准。值得看的重点从模型能否讲出漂亮推理，转向它能否交付可复跑构建、证明依赖和核验工具链；数学家、形式化验证社区和科研Agent团队都会沿着这个标准继续追问。

今天新增了什么

这条新闻的news peg很明确：9月4日，Anthropic发布研究博客，并通过官方X账号指向博客和GitHub仓库。官方X帖的措辞是，Claude上月完成了费马大定理的first formalized proof，证明总计超过1300万行代码，并覆盖证明需要的2.9万多个相关定理。博客正文进一步把口径写细：Claude在11天内完成端到端、computer-checked proof，过程中证明30300个定理，最终证明使用29500个中间定理。

这更接近一项多Agent证明工程，不是单轮模型答题实验。Anthropic描述的流程是多个Claude agents定义概念、证明中间定理，再用这些定理去证明更难的命题。早期尝试失败过，原因包括agent很快丢失项目状态、协作失效；那些失败尝试最终贡献了非样板代码约7%的行数。成功转折发生在切换到Prove2Me之后，这个平台用定理陈述的有向无环图来维护任务状态，并把定理陈述和证明拆分到不同文件中以加快Lean编译和降低资源消耗。

GitHub仓库让这件事从新闻稿变成可检查对象。README开头说明，这是一个基于Lean 4和Mathlib的完整机器核验证明，工具链固定为Lean 4.33.1、Mathlib v4.33.0。顶层声明是自然数版本的费马大定理：对于任意n >= 3，不存在正自然数a b c满足a^n + b^n = c^n。FinalCheck.lean还从这个定理推出Mathlib自己的FermatLastTheorem表述。

仓库提交记录也给了时间锚点。GitHub Atom显示主分支在2026年9月3日有提交，说明这是把证明移植到Lean 4.33.1和Mathlib v4.33.0的版本；提交说明还写到，它是从最初在Lean 4.30.0上检查通过的证明移植而来，约9200个模块文本有变化，但定理、依赖公理和论证结构未变。9月4日的新增是公开披露和发布工件，整个数学工作并非只在当天发生。

关键数字怎么读

指标	官方口径	能说明什么	不能直接推出什么
Claude工作时间	11天	Anthropic称多Agent流程在不到两周内完成端到端形式化	不能推出没有人类设定方向或提示
Lean代码规模	1300万行	这是一个极大规模的机器可检查证明工件	代码越长不等于人类越容易审读
过程中产出定理	30300个	Agent沿途生成大量可验证中间结果	不代表每个命名都符合人类数学直觉
最终使用中间定理	29500个	最终证明依赖的中间定理数量	不能简单等同于新增数学定理数量
输出token	约60亿	该流程是高消耗长程Agent工程	不能直接换算成公开API账单
标准公理	3个	最终依赖propext、Classical.choice、Quot.sound	不等于读者无需审查命题语义
独立核验声明	1052234个声明	README称nanoda接受同一环境导出	仍需社区复跑和长期维护反馈

这些数字里最值得关注的是“最终使用29500个中间定理”和“过程中产出30300个定理”的差异。前者描述最终证明依赖路径，后者描述整个过程中生成的可验证定理池。把两者混在一起，会误导读者以为所有产物都进入了最终证明。Anthropic正文也把这两个数字分开写，本文保持同一口径。

1300万行同样要小心理解。Anthropic称这超过Mathlib五倍；README也说这些Lean源文件用于机器检查，并非面向人类阅读优化。仓库里的名称带有P2M或十六进制后缀，它们是流水线标签，并非数学概念名。README明说，若名称和Lean statement不一致，应以statement为准。这一点对数学审查很关键：机器能检查逻辑依赖，但不能自动保证每个英文名称都准确表达了人类数学含义。

仓库如何证明“可检查”

GitHub README给出三层核验，第一层是Lean本身。从零执行lake build时，Lean kernel会检查仓库的60475个模块，每个声明都要通过内核。FinalCheck.lean包含一个#guard_msgs检查，要求fermat_last_theorem只依赖[propext, Classical.choice, Quot.sound]这三个Lean标准公理。README还写明，仓库模块不包含axiom、sorry、native_decide、unsafe、extern、implemented_by、partial def或#eval；用于挑战的Challenge.lean有意使用sorry，但不属于包内容。

第二层是leanprover/comparator。README称comparator v4.33.0用verification/comparator/Challenge.lean对比证明，确认被证明的statement和它提到的常量与Mathlib-only challenge相同，没有其他公理，而且整个证明连同Mathlib都通过Lean kernel重放，结果为Your solution is okay!。这解决的是“证明表述是否对应费马大定理”这一类等价性问题，范围超过“仓库里有一个叫费马大定理的定理名”这种表面核查。

第三层是nanoda。README称nanoda 0.4.13这个Rust写成的独立Lean kernel实现接受了同一环境的导出，输出为Checked 1052234 declarations with no errors。Anthropic也披露，他们给nanoda打了四个小补丁，一个用于进度输出，三个用于加快定义相等搜索；README强调这些补丁没有增加、删除或削弱类型规则。这个细节很重要，因为形式化证明的可信度不应只依赖单一工具链。

复跑成本也不小。README写到，构建需要Linux或macOS、elan和网络连接；由于没有匹配的预编译Mathlib，需要从源码编译。官方环境下Mathlib约13分钟在96 jobs下编译，完整构建需要每个并行job约5GB内存，.lake/下约67GB磁盘，另有可删除的C文件约220GB；Anthropic自己的构建耗时5小时32分钟，96 jobs峰值153GB内存。comparator约14小时46分钟，峰值230GB，建议预留300GB。这意味着“可核验”并不等于“任意笔记本当天就能轻松复跑”。

Prove2Me扮演了什么角色

Prove2Me早于这次9月4日发布。arXiv条目显示，论文Prove2Me: An Open Collaborative Platform for Scaling Math Formalization最早提交在2026年8月28日，v2更新时间是2026年8月31日。论文摘要说，Lean等证明助手承诺形式化数学，但大型形式化项目门槛高，需要同时懂证明助手和底层数学；AI coding agents降低了自然语言到Lean证明的门槛，于是Prove2Me试图让人类和AI agents在互联网上协作完成形式化任务。

Anthropic的博客把Prove2Me说成这次从失败到成功的关键工程系统。它维护定理陈述的DAG，让agents决定下一步应该尝试证明什么；它把statement和proof分离到不同文件，用独立链接维护依赖，从而降低编译和资源开销；它还给每个定理陈述维护自然语言描述，使搜索和复用更容易。换句话说，Prove2Me处理的是长程协作时最容易崩掉的状态管理、依赖复用和并行调度问题，不只是在回答“模型会不会数学”。

这也解释了为什么Anthropic会强调“dozens of Claude agents collaborated”。如果一个证明任务需要数万中间定理，单个对话窗口很难持续记住全局状态。DAG化的任务池、可复用的中间结果和可检查的Lean构建，才让多Agent协作从聊天接力变成工程流程。对AI研究者而言，本次事件至少提供了一个清晰信号：数学形式化的瓶颈正在从单步证明能力，转向任务分解、状态持久化、失败回收和构建系统。

同时，Prove2Me的角色不应被夸大成“它本身证明了费马大定理”。它是协作平台和harness背景，证明工件在Anthropic公开的仓库里，验证口径由Lean、comparator和nanoda承担。本文把Prove2Me归为关键基础设施，9月4日的新闻主体仍是Anthropic工件公开。

Imperial项目和人类数学背景

Anthropic正文明确提到，Kevin Buzzard在Imperial College London于2024年发起多年的社区努力，希望用Lean完成费马大定理形式化。Imperial项目页也写明，这是一个ongoing multi-author open source project，目标是在Lean theorem prover中形式化费马大定理证明，由Kevin Buzzard领导，并由英国EPSRC资助、Imperial托管。这个项目的重要性在于，它为人类形式化路线、蓝图和部分材料提供了长期基础。

GitHub README和formalization.yaml进一步说明，Anthropic仓库的部分内容来自Imperial College London FLT project、flt-regular和Mathlib，均按Apache-2.0许可归属并在NOTICE和ATTRIBUTION.md中列出。README写到，源自Imperial项目的内容包括Frey package、Galois representations、deformation theory、patching等，ATTRIBUTION.md逐文件列出上游来源和作者。

证明路线本身有清楚来源。PROOF-PATH.md写明，论证来自Frey、Serre、Ribet、Wiles和Taylor-Wiles，并大体遵循Darmon、Diamond和Taylor的 exposition，以反证法运行。路线包括把FLT化约到素数p >= 5、构造Frey package、证明Frey表示不可约、证明半稳定曲线模性、做level lowering，并最终用S₂(Γ₀(2)) = 0关掉矛盾。文件还逐项说明命名经典定理被证明到什么强度，例如Mazur部分只证明Frey曲线需要的不可约性，范围小于Mazur所有有理同源或扭点定理的完整版本。

这个边界对于读者理解非常重要。Claude没有“重新发明现代数论”，它是沿着已知人类证明路线和已有形式化材料，把足够多的缺失环节编码进Lean。恰恰因为目标是已知定理，机器核验才有清晰对照：最终statement是否对应Mathlib里的FLT，依赖公理是否只有标准三项，证明是否能被独立kernel接受。

这件事为什么重要

从数学史角度看，费马大定理的象征意义很强，但AI行业应该把注意力放在验证路径。自然语言证明的可信度长期依赖专家审稿。Anthropic官方页也提醒，大型数学证明的核验可能要耗费数月甚至数年；Wiles在1993年讲授初稿后，也是在密集核查中暴露出关键缺口，最终经过修补才在1995年发表。证明助手提供的是另一种信任结构：只要形式化statement正确、依赖公理清楚、kernel可信，证明链条就能被机械检查。

这对AI生成科学结果尤其关键。随着模型生成更多论文、猜想、证明和实验方案，人类专家的审稿能力会成为瓶颈。形式化证明不能替代人类可读解释，也不能告诉我们一个方向是否有价值，但它可以回答一个更窄、更硬的问题：在给定形式系统里，这个结论是否从这些公理和定义推出。Anthropic这次展示的，就是把一个超级长链的人类已知证明压进这个硬问题里。

对AI Agent工程来说，事件的启发同样明确。一个11天、约60亿输出token、多Agent协作的项目，要求模型长期处理依赖、上下文、构建错误、失败路径和资源约束。它和一次性benchmark很不一样。很多AI应用现在也卡在类似位置：单步能力够强，但多天任务、多人协作、工件复用和回归验证很容易散掉。Prove2Me之所以关键，是因为它把“下一步证明什么”变成可查询、可复用、可并行的状态系统。

对数学社区来说，最值得期待也最需要谨慎。积极的一面是，形式化门槛如果真的被AI降低，更多经典结果、教材定理和新论文可以附带机器核验证明。审稿人可以少花时间查低层逻辑错误，把精力放到概念、动机、命题选择和数学意义上。谨慎的一面是，机器生成的证明可能极长、命名不友好、路径非人类直觉；它能通过kernel，不代表人类已经理解每个中间对象为何这样设计。

接下来要看哪些验证点

第一，独立复跑会决定这件事的社区可信度。README已经给出lake build、comparator和nanoda脚本，但也诚实标注了资源开销。接下来需要看Lean社区、数学形式化团队或大学实验室能否在自己的机器和自己的日志下重现同样结果。如果复跑顺利，Anthropic的“公开工件”价值会明显上升；如果复跑遇到环境、依赖或资源问题，新闻仍成立，但可用性会打折。

第二，要看数学家如何审查语义强度。PROOF-PATH.md已经逐项说明命名经典步骤证明到什么程度，例如Mazur、Langlands-Tunnell、modularity lifting、Wiles和Ribet都只覆盖证明FLT路线所需的强度，没有覆盖“通用版本全证明”。这样的限定是好事，因为它把可证明范围写清楚；后续审查要看的，就是这些Lean theorem的statement是否足够对应传统论证中的关键环节。

第三，要看Anthropic是否公开更多过程材料。官方页给了Claude thinking摘录，也说明人类输入限于偶尔的高层指令，例如“Jacobian as a scheme sounds high priority”等。但要评估AI自主性，还需要更细的任务日志：失败任务如何处理，哪些中间定理由人类改写，DAG如何调度，重复证明如何去重，构建失败如何回滚。没有这些材料，“largely autonomously”仍然是官方描述。

第四，要看Prove2Me能否承接更广泛的协作。Anthropic说，他们还用三个个人Claude Max计划，在Prove2Me上三天完成了Vinogradov’s Three Primes Theorem相关应用的形式化。这个补充很有意思，因为它暗示类似流程不必永远依赖内部研究模型和极大预算。但这一说法仍来自Anthropic，需要看Prove2Me公开平台上的任务、产物、成本和复现情况。

第五，要看这套路径能否走向新结果。形式化已知定理的价值很大，它能降低验证成本、补齐数学库、训练模型处理复杂依赖。但AI数学的更高门槛，是给出新定理、新证明或新工具，并同时附上可核验工件。费马大定理这次是一个标志性压力测试；下一阶段的判断标准，应从“能否复现经典证明”转向“能否稳定把新研究转成可信制品”。

本次写作的来源边界

• Anthropic Research和Anthropic官方X帖是9月4日news peg的直接来源。
• GitHub README、PROOF-PATH和formalization.yaml用于核对证明工件、验证路径、许可、声明强度和复跑要求。
• Prove2Me arXiv论文是8月背景，用来说明协作平台机制，不作为9月4日新增事件。
• Imperial College London FLT project是2024以来的长期背景，用来说明人类形式化路线和部分上游材料。
• 本文没有把“机器可检查”写成“无需人类审读”，也没有把“Claude完成形式化”写成“Claude发现新数学证明”。