AI 11天攻克费马大定理，数学证明进入机器时代

近日，Anthropic 宣布其 AI 模型 Claude 在 11 天内完成了费马大定理的完整形式化证明，写下了约 1300 万行 Lean 代码，过程中人类仅提供少量高层指导。这一成果意味着，原本预计耗时数年的数学验证工程，如今被 AI 压缩至不到两周，数学界为之震动。完整证明已发布于 GitHub，供全球研究者查验。

费马大定理是数学史上最著名的猜想之一，由法国数学家费马于 1637 年提出，断言当整数 n 大于 2 时，方程 aⁿ+bⁿ=cⁿ 无正整数解。该猜想在 1995 年由安德鲁·怀尔斯与理查德·泰勒修补关键缺口后正式证明，但验证大型数学证明传统上高度依赖人类审稿人，过程漫长且易出错。Claude 并未提出新的证明路线，而是将怀尔斯 1995 年发表的 129 页现有证明，转写为机器可逐步核验的 Lean 代码，这本身就是一项浩大工程。

从纸面到机器：形式化证明的挑战

形式化证明通过 Lean 等证明助手，依据明确公理逐步检查逻辑，补全人类可省略的步骤。此次工程沿用了 Henri Darmon、Fred Diamond 和 Richard Taylor 整理的简化证明路径。数十个 Claude 智能体并行协作，共完成 30300 个定理的机器可验证证明，其中 29500 个进入最终版本。工程消耗约 60 亿个输出 Token，规模超过 Lean 核心数学库 Mathlib 的 5 倍。Lean 检查确认，证明仅使用其三条标准公理，且所证定理陈述与 Mathlib 中的一致，确保了结果的可靠性。

Prove2Me 平台：协作的关键

工程的成功得益于 Prove2Me 平台。该平台将待证定理组织成有向无环图，记录任务依赖关系，帮助智能体掌握全局进度并复用结果。早期实验中，多个智能体因无法有效协作而失败，最终证明中约 7% 的非模板代码来自这些失败尝试。Prove2Me 将定理陈述与证明拆分管理，缩短了编译时间，使得大规模并行协作成为可能。

帝国理工学院数学家 Kevin Buzzard 审阅后认为，这表明 AI 自动形式化已能处理大型现代数学工程，有助于发现证明错误并减轻审稿人负担。但机器验证也有边界，Lean 能确认逻辑正确性，却无法提供直觉清晰的解释。未来数学成果或需同时具备面向研究者的思路阐述与面向机器的可核验版本。

Anthropic 另进行的小规模实验显示，三个个人版 Claude Max 账号通过 Prove2Me 协作，三天内完成了维诺格拉多夫三素数定理的形式化，表明类似工作未来或可扩展至普通研究团队。从费马大定理到三素数定理，AI 正在将数学验证从“人类审稿”推向“机器核验”的新阶段，这或许预示着数学研究范式的深刻变革。