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独立发现新证明或新数学结果。人类数学家的原始洞察与证明结构仍是基础。

对数学界的可能影响

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