Claude用11天形式化费马大定理：证明已开源，不是重新发现

Anthropic于2026年9月4日公布Claude用11天完成的费马大定理Lean 4形式化成果，并开放证明代码。Tech Times 9月5日的报道 核对了发布日期、工期和成果性质：Claude处理的是安德鲁·怀尔斯与理查德·泰勒既有论证的形式化，不是一项取代人类工作的数学新发现。

Anthropic的研究说明 称，Claude在多智能体系统中大体自主工作11天，写出约1300万行Lean代码，共完成30300个中间定理的机器可检查证明，其中约29500个用于最终证明；这次运行还消耗约60亿个输出令牌。上述工期、代码量和令牌量均为发布方披露的项目数据，而不是第三方重跑后得到的测量结果。

新成果是完整形式化，不是重新解决定理

费马大定理早已由人类证明。此次工作的新增部分，是把既有证明路径转换成Lean能够逐步读取和核验的精确表达，并把最终陈述与所需中间环节接入同一条形式依赖链。

项目沿用Frey、Serre、Ribet、Wiles和Taylor—Wiles的论证体系，主要遵循Henri Darmon、Fred Diamond与Richard Taylor给出的简化阐述，同时使用Mathlib以及伦敦帝国理工学院FLT项目、flt-regular项目的既有成果。“端到端”意味着最终定理可以沿形式依赖追溯到底层定义和证明项，并不意味着Claude从零创造了这些数学思想或基础库。

数学证明、证明形式化和机器检查并不是同一个动作。数学家撰写的论文可以省略同行熟悉的步骤；形式化必须明确写出定义、类型、前提和推理；机器检查则由Lean内核判断这些形式表达是否确实遵循规则。Claude主要完成第二项工作，并生成了可供第三项工作处理的证明对象。

Lean检查的是逻辑链，而不是数学原创性

Lean内核检查的核心问题是：在指定定义、公理和已有证明项之下，目标结论是否能够合法推出。检查通过说明形式系统没有在推理链中发现缺口，但不会判断某个证明思路是否新颖，也不会自动决定中间定理的名称是否准确概括其数学含义。

因此，把结果简称为“Claude证明了费马大定理”容易混淆两种含义。从形式逻辑看，Claude确实构造了一份可由内核接受的完整形式证明；从数学发现史看，它编码和补全的是已有路线，没有首次解决一个尚未解决的猜想。发布方所谓的新意，是首次完成这项端到端机器检查，而非发现新的费马大定理证明思想。

机器检查也不是脱离软件条件的绝对保证。结论仍以Lean或其他检查内核、导出程序和比较工具的正确实现为前提；形式化能够显著减少对人工逐行判断的依赖，却不能替代对定义选择、数学含义和来源归属的审读。

开源仓库能够复核，但重建成本不低

公开的完整证明仓库 采用Apache 2.0许可证，固定使用Lean 4.33.1和Mathlib v4.33.0；最终定理覆盖自然数指数n≥3及正自然数a、b、c，并限定证明依赖propext、Classical.choice和Quot.sound三项标准公理。仓库记录显示，从源码构建的60475个模块全部通过Lean内核检查；comparator确认最终陈述及其引用常量与Mathlib挑战陈述一致，Rust实现的独立内核nanoda 0.4.13又接受了同一环境中的1052234项声明。团队为nanoda加入四个补丁，其中三个用于加速定义相等性搜索，并说明这些补丁未改变类型规则。

仓库同时提供FinalCheck.lean、PROOF-PATH.md、来源归属记录、验证脚本和可离线浏览的证明页面。公开内容不仅能让外部研究者查看最终结论，还能追踪中间定理、依赖关系及复用的上游代码；不过该仓库被标记为不维护、不接受贡献的研究制品。

发布方列出的参考构建需要Linux或macOS、网络连接和elan，并要求从源码编译Mathlib。其一次96并行任务构建耗时5小时32分钟，峰值内存153 GB，构建目录约占67 GB，过程中生成的C文件还可能额外占用约220 GB；comparator重放则耗时14小时46分钟、峰值内存230 GB。这些是特定硬件与并行配置下的报告值，不能视为其他设备必然得到的结果。

11天和1300万行说明了什么

11天并非单个聊天会话连续推理的时间。项目由数十个Claude智能体协作，并使用Prove2Me维护定理陈述及其依赖构成的有向无环图；智能体据此选择待完成节点、查找已有结果并共享项目状态。此前的尝试曾因智能体逐渐丢失整体状态而失败，改用这一协作结构后才完成整个依赖链。

约1300万行首先是工程规模指标，不是数学原创性的计量单位。Lean要求显式写出人类论文会省略的细节，而机器生成的代码也可能远长于经过人工整理的形式证明；发布方自己亦指出，该成果很可能比必要长度更长。类似地，约60亿个输出令牌表明这是资源密集型研究项目，但由于没有公开可直接核算的总成本，不能据此宣称普通Claude订阅可以用同样条件重演全过程。

目前能够核实的状态是：证明代码已经开放，固定工具链下的全量构建、陈述比较和第二内核检查均由仓库记录为通过，数学路径与上游来源也可供审查。接下来仍需独立团队在不同硬件上重建制品、检查庞大的依赖链及补丁，并对形式陈述的数学含义进行更深入的人类审读；这项成果改变的是大规模形式化的速度，而不是费马大定理的发现史。