发生了什么
Anthropic 于当地时间 9 月 4 日发布研究公告：其 AI 模型 Claude 在 11 天内基本自主完成了费马大定理的端到端形式化证明，这是该定理首个完整、经计算机检查的证明文件。费马大定理由皮埃尔·德·费马于 1637 年提出，断言对任何整数 n 大于 2，不存在正整数 a、b、c 满足 a 的 n 次方加 b 的 n 次方等于 c 的 n 次方；英国数学家安德鲁·怀尔斯于 1995 年给出长达 129 页的首个正确证明。此次 Claude 并非重新发现证明，而是将怀尔斯证明（遵循 Darmon、Diamond 和 Taylor 的简化阐述）翻译成 Lean 证明助手可逐步验证的严格逻辑形式。
工程规模与协作方式
- Claude 生成约 1300 万行 Lean 代码，证明约 3.03 万个定理，其中约 2.95 万个中间定理被纳入最终证明，整体规模超过 Mathlib 数学库的 5 倍
- 项目消耗约 60 亿输出 Token，使用一个与 Claude Fable 5.1 大致相当的通用内部研究模型
- 多个 Claude 智能体借助彭天翼团队开发的 Prove2Me 平台并行协作，该平台以有向无环图（DAG）记录定理依赖关系并支持分工复用
- 人类研究者的输入以高层指令为主（如确定数学对象与定理的优先级），具体证明过程主要由 Claude 完成
- 证明通过 Lean 完整检查，仅依赖 Lean 的三条标准公理；项目另用 Comparator 流程及 Rust 独立实现的 Nanoda 内核进行了第二轮验证
为什么重要
数学形式化一直被视为以年为单位的大型工程：伦敦帝国理工学院教授 Kevin Buzzard 2024 年发起的社区项目曾计划用数年时间完成同一目标，仅第一阶段技术蓝图就达 86 页。Claude 的成果表明，AI 已能把跨越代数、调和分析、几何与数论等多个分支的庞大证明工程，推进到机器可验证的完整形式。Buzzard 审阅后评价称，该证明除数学公理外不依赖任何额外假设，AI 自动形式化产物已达到可被继续构建的稳健程度。Anthropic 认为，随着 AI 生成数学成果增多，为面向人类阅读的证明同步提供形式化版本可能成为常见做法，从而减轻数学成果验证与同行评审的负担。
尚存的不确定性
需要审慎看待的是：此次工作的新意在于端到端机器验证，而非提出新的数学证明；仓库中 106 个文件包含取自帝国理工 FLT 项目等既有来源的文本，且人类数十年积累的数学基础设施是重要前提。此外，独立复验门槛较高——源码构建峰值内存约 153 GB，Comparator 检查接近 15 小时、峰值约 230 GB；项目评审状态仍为自我评估，验证日志尚未完整公开。对依赖 AI 的企业而言，该案例展示的「生成模型 + 严格形式验证器」组合在数学这类具有明确判定标准的领域成效显著，但能否迁移到规范模糊的商业软件场景，仍有待观察。完整 Lean 证明已公开于 GitHub（anthropics/fermats-last-theorem）。