Claude据称用11天完成费马大定理的Lean形式化

Anthropic表示，Claude已经产出了费马大定理（FLT）首个完整、端到端、可由计算机检查的Lean形式化版本。需要先厘清一点：Claude并没有发现费马大定理的新证明。它所做的是把一条已经确立的现代证明路线，转化为Lean能够机械核验的庞大形式化成果。Anthropic称，这项工作历时约11天，主要由智能体自主完成，最终生成约1300万行Lean代码。215

被形式化的到底是什么？

费马大定理指出：当指数 (n\ge 3) 时，方程 (a^n+b^n=c^n) 没有非平凡的自然数解。Mathlib——Lean生态中广泛使用的形式化数学库——将其表述为：只要满足该方程，则 (a)、(b)、(c) 至少有一个为零；这与人们熟悉的“没有正整数解”的说法等价。31

该项目沿用的是Darmon–Diamond–Taylor版本的Wiles／Taylor–Wiles证明策略，而非提出新的数学路线。这一区别很关键：传统论文可以略去许多“由标准论证可得”的连接步骤；形式化证明则必须明确写下定义、前提、辅助结论及每一段推理的衔接。帝国理工学院的FLT形式化项目也将其路径描述为Wiles／Taylor–Wiles证明的现代变体。511

1300万行代码从何而来？

证明助手不会接受“显然”或“由标准方法可得”。每一项推论都必须以系统可类型检查的形式表达，并且所依赖的结果也必须已经被形式化。

Anthropic称，项目共生成约30,300个经计算机验证的定理，其中约29,500个进入最终证明的依赖闭包。整个开发横跨代数、几何、调和分析和数论等领域。215

因此，“11天”不应被理解为用11天取代了费马大定理漫长的数学史。Anthropic还称，运行过程生成了约60亿个token；其中包含大量候选证明、Lean检查、根据报错进行修补，以及组织超长形式化项目所需的工程工作。5

核心不是单个模型，而是多智能体协同

这项结果据称并非依靠一个模型在单一上下文中始终记住整份证明。Anthropic表示，早期尝试虽有进展，却难以维持共享的项目状态；成功的一轮运行采用了基于Prove2Me的平台和运行框架。Prove2Me旨在支持协作式数学形式化。529

其组织核心是一张有向依赖图：

• 节点对应尚待完成的定义、引理或定理；
• 边表示后续结果依赖哪些前置结果；
• 智能体可挑选尚未解决且有用的任务，在Lean中完成证明，并将成果交给其他智能体复用；
• 系统再从基础组件逐层推进，直至最终定理。

Prove2Me将这种协作称为发起形式化“任务”，由智能体贡献可复用的形式化证明。29 这种依赖图机制把一项漫长而脆弱的任务拆成许多可独立核验的子问题，也将项目记忆保存在模型单次运行之外。

“计算机核验”具体保证了什么？

Anthropic称，最终项目不含Lean中的sorry占位符——即没有把未证明结论直接当作成立使用——并且只依赖Lean的三条标准公理。5

这远强于AI写出一段看似有说服力的自然语言证明。Lean的内核会检查每一步编码后的推理，确认其是否遵循系统的逻辑规则、公理和已导入依赖项。Anthropic还称，已核对最终结论与Mathlib中既有的FermatLastTheorem表述一致。531

但内核检查也有清晰边界：它验证的是被写入系统的形式化命题。形式化定义和中间命题是否忠实对应人们意图中的非形式化数学，仍须由人类判断。因此，独立编译公开成果、审计依赖链，以及由相关领域专家审阅，都是检验这项声明的重要环节。

为什么Kevin Buzzard称其“非同寻常”

据Anthropic的报道，帝国理工学院数学家Kevin Buzzard将这一成果称为“非同寻常的自动形式化成就”。21 其意义不只在于智能体能够做完若干独立的Lean习题，而在于它们据称构建了一个层级极深、可复用、覆盖多数学分支的形式化开发成果——过去人们通常预期这需要协调良好的人类团队投入多年时间。

若这类工作能够稳定复现并降低成本，数学形式化可能带来几项实际价值：

• **更严格的核查：**形式化系统可暴露论文叙述中难以发现的遗漏前提、无效变换或定义不匹配；
• **可复用的基础设施：**一个引理一旦完成形式化，后续项目可直接导入，并依靠内核核验其逻辑有效性；
• **补充同行评审：**机器可核查的证明有望减轻审核超长技术论证的负担，同时由数学家继续判断问题的含义、重要性和证明策略。

这些是潜在收益，并不意味着数学判断会被自动取代。一个形式化证明即使逻辑上有效，也可能形式化了错误的命题；而1300万行代码和数十亿token所反映的计算与工程成本，目前仍然很高。

应当如何解读这项声明？

这项据称完成的FLT形式化，是AI辅助形式化的重要基准：目标定理早已被证明，最终成果则旨在让外部独立检查。它不应被描述成“Claude新解决了费马大定理”。

更准确、也更有影响力的表述是：Anthropic称，一个协调式智能体系统利用依赖图分解任务与形式验证反馈，将一项重大既有证明转写成了前所未有规模的Lean开发成果。21529

接下来真正值得关注的问题是：外部研究者能否复现构建、审查其形式化含义、复用其中组件，并在其他高阶数学课题上得到可比结果。答案将决定这是一项一次性的工程壮举，还是现代数学构建与核查方式的持久转变。