Claude 用 11 天「验完」费马大定理：AI 证明数学的里程碑

一句话说清：Anthropic 宣布，AI 模型 Claude 基本自主运行 11 天，完成了「费马大定理」第一个端到端、经计算机检查的正式证明——相当于 AI 把人类几百年才证出的数学定理，用机器能逐行验证的方式重新走了一遍。

发生了什么

• 9 月 4 日，Anthropic 宣布其模型 Claude 在约 11 天的基本自主运行里，完成了费马大定理（FLT）首个端到端、经过计算机检查的形式化证明。
• 这不是「重新发现」数学证明，而是把怀尔斯 1995 年的证明，转换成 Lean 证明助手能一步步验证的形式（Lean 是专门用来写和校验形式化数学证明的工具）。
• 规模惊人：Claude 生成约 1300 万行 Lean 代码，证明了约 3.03 万个定理，其中约 2.95 万个中间定理被纳入最终证明；整套证明只用了 Lean 的 3 条标准公理，由 Lean 内核完成检查。
• 方式是多智能体协作：项目由 Anthropic 研究员 Tianyi Peng（清华姚班校友）发起，用 Prove2Me 平台把大证明拆成有向无环图，几十个 Claude 智能体并行认领子任务。
• 数学界反应冷静：帝国理工的 Kevin Buzzard 自己编译验证后说，这项工作「在数学上几乎没告诉我们新东西」——重点不在发现，而在自动验证。

来源：IT之家/今日头条（2026-09-05）、AI Bacon（2026-09-05）、Sohu、ExplainX 报道。

对我有什么用

• 这是 AI 在「形式化数学验证」上的标志性一步：过去专家预计这类工作要数年，Claude 用 11 天跑完，说明多智能体 + 证明助手能大幅压缩大规模验证的成本。
• 意义在「基础设施」：未来新数学证明越来越多，AI 辅助形式化可以降低人工审稿负担，让数学结论更可靠、可复现。
• 也再次证明前沿模型的能力边界在快速外扩——从聊天、写代码，到参与严谨的逻辑推理。

我可以怎么做

1. 当故事看趋势：这不代表 AI 马上能替你做数学作业，但说明「AI + 验证工具」正在进入严肃领域，值得关注。
2. 借力学逻辑：Lean、Prove2Me 这类形式化工具对编程/数学感兴趣的人是好入口，能边玩边理解「什么叫能被机器验证的正确」。
3. 理解 Agent 协作：这个项目是「多智能体并行干活」的范例，和你用 AI 编程、AI 办公的思路相通——把大任务拆小、分给多个 AI。
4. 别神化：Anthropic 自己也说，这次新意在于「验证」而非「发现」，AI 离独立提出重大数学突破还有距离。

温馨提醒

• 不是 AI 自己「想出」证明：是人类已有证明的形式化重写，AI 负责把每一步变成机器可验的代码。
• 别拿它当解题神器：日常数理化作业请用常规 AI 辅导工具，这类形式化证明对普通人暂无直接用途。
• 涉及学术/考试诚信，AI 生成的证明或作业要符合学校和使用场景的规定。
• 数字有细微出入（不同来源统计 2.95 万~3.03 万定理），属正常计数口径差异。