Claude用Lean完成费马大定理形式化：真正的进步是让证明可核验

2026年9月4日，Anthropic宣布，Claude智能体用约11天完成了费马大定理在Lean 4中的一套完整形式化。该公司称，这是这一定理首个由计算机完整核验的形式化成果，整个过程大体由智能体自主完成。真正值得关注的，不是人工智能“重新证明”了一道悬而未决的难题，而是它把一套早已成立、内容极其庞杂的现代数学论证，整理成了证明助理能够逐步检查的形式。

这一区别很重要。费马大定理早已由怀尔斯以及泰勒—怀尔斯的工作解决；此次成果沿用弗雷、塞尔、里贝、怀尔斯和泰勒—怀尔斯奠定的证明路线，具体遵循经典的达蒙—戴蒙德—泰勒论述。它汇集了几代数学家的成果，也离不开人类此前建设的形式化数学程序库。因此，它既没有为费马大定理增添新的数学结论，也不等于人工智能独自攻克了一个开放问题。

不过，“没有提出新证明”并不意味着没有进步。传统数学论文可以把公认事实、常规推导和大量背景知识浓缩在几句话里；证明助理却要求关键环节最终写成内核能够核验的精确表达。要把一条横跨多个数学领域的漫长论证纳入这样的严格体系，必须处理海量定义、引理和依赖关系，本身就是规模惊人的知识工程。此次发布的积极意义，正是自动化系统开始能够承担其中相当一部分繁重工作，而成果又以代码仓库的形式开放给外界检查。

一句话背后的庞大依赖网络

仓库中的最终命题与通常表述一致：当自然数n≥3，且自然数a、b、c均为正数时，aⁿ+bⁿ不等于cⁿ。表面上只有一句话，真正写进证明助理时，却要把它调用的定义、引理、数学结构以及彼此之间的关系逐一落实。

Anthropic公布的数据让人看到这项工程的体量：整个产物约有1300万行Lean代码，模型生成约60亿个输出词元，共证明约30300项中间结果，其中约29500项用于最终证明。仓库清单还按另一套统计口径列出29511个定理页面、1450个定义模块和60475个已构建模块。这几组数字衡量的对象不同，不能合并成一个所谓的“定理总数”；它们共同反映的是，最终那句简洁的结论依托着一个极其庞大的形式化网络。

60亿个输出词元也不能直接换算成实际费用或能源消耗。公开资料没有提供完整的成本账目，因此任何看似精确的金额或能耗估算都缺少依据。约11天的运行时间显示了系统推进任务的速度，却不足以单独说明效率高低。若要作出全面比较，还需要知道所用计算资源、失败尝试的数量、人工如何介入，以及后续维护需要付出多少成本。

关键不是模型有多自信，而是结果能否复核

形式化证明的价值，不取决于语言模型如何评价自己的答案，而取决于结果能否交给规则明确、范围较小的检查机制。该项目固定使用Lean 4.33.1和Mathlib v4.33.0，以免软件版本变化使核验条件变得含糊。仓库的默认检查还要求最终定理所依赖的公理恰好是propext、Classical.choice和Quot.sound。明确软件版本和公理依赖后，“通过检查”就成了可以重复验证的技术主张，而不只是一句宣传口号。

仓库还声明，项目模块没有使用axiom、sorry、native_decide、unsafe、extern、implemented_by、partial def或#eval；另附的挑战文件有意使用sorry，但不属于软件包本身。这些是仓库给出的说明和构建保障，并不等同于外部人员已经逐行审阅了1300万行代码。这样的限定不能省略：它说明现有证据究竟支持到哪一步，也为进一步复查留下了明确入口。

项目报告称，comparator v4.33.0核对了挑战命题是否完全一致、公理限制是否满足，并让Lean内核重新检查证明，最终返回“Your solution is okay!”。数学家Kevin Buzzard也独立编译了代码并运行comparator，确认结果能够通过检查。这是对仓库可构建性和比较器验收结果的有力旁证，但不能扩大解释为每个抽象设计、定理命名和数学说明都经过人工审查。

项目方还报告说，由Rust编写的另一套Lean内核实现nanoda 0.4.13接受了包含1052234项声明的导出文件，没有报错。Anthropic为nanoda应用了四个补丁，并称这些改动只涉及进度显示和搜索性能，不改变类型检查规则。第二套内核的结果增加了一层验证，不过这一结果仍由项目方报告，相关补丁也理应接受独立检查。

机器核验同样不代表今后什么都不必信任。它证明的是：在指定定义、公理和可信计算基础之下，那条精确的Lean命题可以按规则推导出来。人们仍须确认形式化命题是否准确表达了原来的数学问题，审视基础公理、内核、编译器和工具链，并考虑软件乃至硬件出错的可能。机器也不会自动判断选题是否有价值、命名是否合理、解释是否清楚，或者代码是否便于维护。更准确地说，形式化把每一步推导必须满足的要求明确记录下来，同时把仍需信任和核查的范围集中到命题表述、公理、内核及工具链等环节。这样一来，问题更容易定位，检查也更容易重复。

更大的意义在于降低形式化门槛

数学形式化长期面临一个实际瓶颈：要把成果纳入证明助理，研究者不仅要懂数学，还得把纸面论述拆成大量精确步骤，解决定义衔接、程序库检索和依赖组织等问题。这项工作重要却耗时，因此许多早已得到数学界认可的成果，仍没有可由机器检查的完整版本。此次项目至少表明，人工智能代理系统能够在超大规模任务中持续生成、连接和核验形式化构件，而不只是解答几道彼此孤立的习题。

如果类似能力在更多项目中得到独立复核，数学家与证明助理之间的分工可能随之改变。研究者可以把更多精力投入命题选择、整体结构、概念阐释和真正困难的环节，让自动化工具处理部分重复而细密的编码工作。可由机器核验的数学资料也更便于检索、组合和重新检查，有望成为教学、程序验证及后续研究的基础设施。

不过，一个规模巨大的成功案例只能证明这种做法已经展现可行性，不能单独证明生成过程足够经济，也不能保证产物天然易读、易维护或适合直接复用。该仓库采用Apache-2.0许可证发布，注明它是一个不再维护、也不接受贡献的研究成果，并说明其中使用了伦敦帝国理工学院FLT项目、flt-regular和Mathlib的衍生材料。庞大而可检查的独立成果，与适合纳入Mathlib、供人阅读和长期维护的程序库代码并不是一回事。Buzzard也指出，帝国理工学院的另一项工作仍在承担程序库建设和数学解释方面的任务。

开放仓库让讨论可以越过宣传口号。外部研究者能够查看定理究竟如何陈述、固定了哪些版本、最终结论依赖哪些公理，也可以重新运行现有检查。今后更有说服力的进展，将来自更多人对构建过程、nanoda补丁、代码结构和维护成本的复核，也来自同类方法在其他大型数学项目中的重复成功。

因此，这条消息最稳妥的积极解读不是“人工智能已经取代数学家”，而是形式化数学最费时的一类工程劳动出现了新的自动化路径。费马大定理没有被再次发现，但一套经典证明被整理成了可重复进行机器检查的公开成果。若这种能力继续成熟，更多重要数学知识就可能从主要依靠专家阅读的文本，转化为既供人理解、又能由工具逐项复核的共同基础。