Anthropic宣布Claude完成费马大定理首个端到端计算机验证Lean形式化证明

2026年9月4日，Anthropic宣布其AI模型（Claude系列）在基本自主运行约11天后，成功完成了对费马大定理（Fermat’s Last Theorem, FLT）的首个端到端、经计算机检查的Lean形式化证明。这项工作并非由AI重新发现该定理的数学证明，而是将已有人类证明（主要基于安德鲁·怀尔斯1995年的工作及其后续阐述）转换为Lean证明助手能够逐步验证的形式。最终成果包含约1300万行Lean代码，证明了约3.03万个定理，其中约2.95万个中间定理被纳入完整证明，且仅依赖Lean的3条标准公理。相关代码已开源至GitHub。⁠Anthropic

详细情况：从人工数年预期到AI十一天完成

费马大定理指出：当整数指数 n>2n > 2n>2 时，不存在正整数 a,b,ca, b, ca,b,c 满足 an+bn=cna^n + b^n = c^nan+bn=cn。怀尔斯于1995年给出的证明长达约100⁠–⁠129页，其正确性曾经历数月人工核查。将此类现代数学证明完全形式化（即写成计算机可逐步检查的代码）长期被视为艰巨任务。帝国理工学院Kevin Buzzard领导的社区项目原计划用数年时间完成FLT的Lean形式化，项目蓝图本身就长达数十页。

Key milestones from the Prove2Me plan that Claude used to formalize Fermat’s Last Theorem. The three colored sections correspond to three core sub‑theorems that Claude had to prove on the way to its final goal. This graph closely follows Wiles’s original proof.

Anthropic研究员Tianyi Peng团队测试Claude在自动形式化上的能力。通过多Agent协作框架（结合Prove2Me等工具），数十个Claude Agent协同定义概念、证明中间定理，并逐步推进更复杂的命题。过程中消耗约60亿输出Token，模型基本自主运行约11天，最终产出完整、可机器检查的证明。该证明规模超过现有Mathlib数学库的五倍，成为迄今最大的Lean证明。

验证方面，证明通过Lean内核检查，使用比较器确认其陈述与Mathlib中的FLT表述一致，且未引入额外公理。GitHub仓库提供了完整代码、证明路径说明及可浏览的HTML版本。

需要强调的是：这是形式化（将已有证明翻译为可验证代码），而非AI独立发现新证明或新数学结果。人类数学家的原始洞察与证明结构仍是基础。

对数学界的可能影响

1. 加速数学文献形式化
2. Buzzard评价称，若FLT自动形式化已可行，则向现代数学文献的自动形式化迈出了一大步。未来可能系统性排查现有文献中的错误、减轻审稿负担，并为进一步数学研究提供更坚实的计算机可检验基础。
3. 改变证明验证范式
4. 传统上，复杂证明依赖专家人工审查，耗时且易有疏漏。机器检查的形式化证明提供更高确定性，尤其适用于长证明与跨领域结果。FLT案例证明，AI已能处理此前被认为需要数年人力的规模。
5. 工具与协作新模式
6. 多Agent分工、中间定理库构建、与现有Mathlib的集成，展示了AI辅助形式化的可行路径。数学家可能更多转向“高层指导 + AI执行细节”的工作流，专注于概念创新而非繁琐形式化。
7. 对数学实践的深远影响
8. 若自动形式化普及，数学研究的可重复性与可信度将显著提升，同时也可能改变教育、发表与合作方式。部分基础性、验证性工作可能被大幅自动化。

人类对AI的忧虑与反思

这一突破也加剧了关于AI能力边界的讨论：

• “理解”与“执行”的界限

AI能将复杂人类证明转化为可验证代码，是否意味着它“理解”了数学？目前更准确的描述是强大的模式匹配、规划与代码生成能力，而非人类式的概念洞察。但当AI能独立完成此前需专家团队数年的形式化工作时，这种区分变得模糊。

• 对数学家角色的冲击

若验证与形式化大量自动化，数学家的核心价值将更集中于提出新问题、构建新框架与创造性洞察。部分人担忧“证明工厂”式工作可能稀释数学的人文与探索特质。

• 可靠性与依赖风险

虽然Lean内核提供了强检查，但AI生成的海量中间步骤是否完全可信、是否存在隐蔽错误，仍需持续独立审查。过度依赖AI可能引入新的系统性风险。

• 更广泛的AGI与就业焦虑

FLT形式化被视作AI在严密逻辑领域的重要里程碑，强化了“AI正快速进入高认知门槛领域”的叙事，进一步引发对科研、教育及知识工作未来的讨论。

结语

Anthropic用Claude在11天内完成费马大定理的端到端Lean形式化，是自动定理证明与AI辅助数学的一个标志性事件。它证明了当前大模型在复杂、长周期、高严密性任务上的执行能力已远超此前预期，同时仍建立在人类既有证明之上。对数学界而言，这既是强大新工具的到来，也是对研究范式与人类角色的重新审视；对公众而言，它再次提醒：AI正在改变知识生产与验证的方式，相关机遇与忧虑需要同步被认真对待。

完整证明已开源，数学与计算机科学社区的独立验证与后续应用，将决定这一成果的真正历史分量。

▶️ 喜欢这篇内容？创作真的很辛苦！

欢迎关注我们的 YouTube 频道：
AI Rosetta

你的点赞、订阅和分享，是对我们最大的支持！🙏

更多AI新闻请访问： https://www.airosetta.com