Claude用11天完成费马大定理的完整形式化

导语

费马大定理的数学证明早在20世纪90年代已经完成，但要把这份证明写成计算机能够逐步核验的形式化程序，仍是一项规模庞大的工程。Anthropic近日披露，研究团队让Claude参与了这一过程，并在约11天内完成了一个端到端的Lean形式化版本。这里的“完成”并不是AI重新发现了费马大定理，而是把人类数学家能够理解的证明，翻译成形式系统不允许跳步的代码。

这次到底完成了什么

费马大定理断言：当整数指数大于2时，不存在正整数a、b、c满足aⁿ+bⁿ=cⁿ。Andrew Wiles在1990年代完成了原始证明，但自然语言数学论文中常会使用“显然”“类似可得”等依赖读者背景的表达。Lean则要求定义、引理、类型和推导关系都明确写出，并由内核检查证明是否能够从既有公理和定理推出。

据Anthropic介绍，该项目生成约1300万行Lean代码，包含3万多个中间定理，最终证明使用其中约2.95万个结果。工程规模超过Lean数学库Mathlib自身的五倍。团队还表示，最终形式化证明只依赖Lean的三个标准公理，并通过程序比对确认其定理陈述与Mathlib中的费马大定理一致。需要注意的是，这些数字和成果目前主要来自项目方披露，文章不应将其等同于AI发现了新的数学理论。

Harness比“多开几个Agent”更重要

项目早期，多智能体虽然能够并行生成代码，却很快丢失全局状态，彼此重复工作，留下的失败代码只占最终非模板代码的一小部分。转折点是引入Prove2Me及基于Claude Code的多智能体Harness。

这套系统把证明拆成由定理节点组成的有向无环图，记录每个节点的前置条件、完成状态和可复用结果；同时分离定理陈述与证明，加速Lean编译，并保留自然语言描述供Agent检索。不同Agent可以分别负责定义、中间引理、后续定理和最终拼装，人类则主要提供方向性提示。项目据称消耗约60亿个输出Token。

意义与边界

这件事的核心价值，是展示AI可能从“回答数学问题”走向“管理形式化数学工程”。如果模型能够持续拆解任务、调用工具、修复编译错误并复用中间成果，过去需要多年社区协作的形式化工作，或许可以获得显著提速。

但Lean只能确认提交的形式化证明在既定基础上成立，不能替代对建模方式、定理陈述和工程流程的审查。更现实的结论是：未来数学AI的竞争，不只取决于模型会不会推理，也取决于任务图、记忆、编译器和协作Harness是否可靠。

来源：量子位