Claude 11天完成费马大定理完整形式化证明 AI数学验证进入工程化阶段

9月4日，Anthropic官方发布研究成果，宣布完成费马大定理首个端到端计算机可验证形式化证明。该工程由Claude模型主导完成，全程历时11天，生成约1300万行Lean证明语言代码，覆盖29500个中间定理，是全球数学形式化领域首个达到工业级规模的公开成果，标志着AI辅助数学验证从零散实验正式进入工程化落地阶段。

数年级工程压缩至11天

费马大定理自1637年提出后，历时358年才由怀尔斯与泰勒完成人类证明，全文129页，横跨代数数论、模形式、伽罗瓦表示等多个细分领域。对其进行形式化验证——即将自然语言书写的证明转化为可由机器基于公理逐行核验的严格逻辑链——是学界近20年的重要目标。2024年帝国理工学院启动社区攻坚项目，仅第一阶段技术蓝图就达86页，行业普遍预计完整工程需数年推进。

此次Claude完整复现了Darmon-Diamond-Taylor版本的怀尔斯证明路径，共证明29500个中间定理，整套证明仅依赖Lean系统的三条标准公理，未引入任何额外假设。最终成果经Lean 4.33.1内核全量编译校验，并由独立的Rust语言Lean内核nanoda交叉验证，确认定理陈述与Mathlib官方版本完全一致。1300万行的代码规模，已超过Lean核心数学库Mathlib的5倍。

多智能体协作的工程化框架

这一成果的核心并非单一模型的推理能力突破，而是构建了一套可复制的大规模数学形式化协作框架。项目早期曾遭遇协作瓶颈：并行工作的智能体无法同步全局进度，难以复用彼此成果，导致推进停滞。

最终的解决方案来自Prove2Me协作平台，由Anthropic研究员彭天一与哥伦比亚大学团队开发。该平台将全量待证定理组织为有向无环图，明确任务间的依赖关系，智能体可自主判断任务优先级，支持长时间并行推进；同时将定理定义与推导过程拆分存储，独立维护关联关系，大幅缩短Lean编译时间与算力消耗；每个定理还匹配人类可读描述，支持智能体语义检索与成果复用。

在该框架支撑下，数十个Claude智能体分层推进，从基础概念定义、中间定理推导到高层结论组装，全程仅接受人类的少量高层方向指引，具体推导与代码生成均由模型自主完成。整个工程消耗约60亿输出token，所使用的内部研究模型能力与Claude Fable 5.1相当。

验证能力升级而非数学原创

需要明确的是，这项工作并未提出新的数学证明路线，其核心价值在于验证范式的工程化突破，而非数学原创性进展。

对数学研究而言，形式化验证可补全人类证明中默认省略的推导环节，排查经典文献中的潜在错误；更可将数学论文数月至数年的审稿周期，压缩至数小时的机器编译校验。随着AI生成数学成果的速度加快，形式化工具更将成为锚定AI可信度的核心支撑，应对未来成果爆发式增长带来的验证瓶颈。

但该技术的边界也十分清晰：当前生成的证明代码冗余度较高，远未达到人工编写的简洁度与可读性，仅能承担验证功能，无法替代人类的数学直觉、思路阐释与价值判断。未来数学研究大概率将形成“人类可读阐释版+机器可核验版”的双轨产出模式。

形式化验证走向规模化复用

这项成果的影响远不止于纯数学领域，它验证了AI驱动的形式化工程具备规模化复制的可能。

Anthropic同步披露的对照实验显示，使用三个个人版Claude Max账号，通过同一套协作框架，仅用三天即完成维诺格拉多夫三素数定理的形式化。这意味着该方法已不再局限于头部实验室，普通研究团队也可依托成熟的任务拆解机制开展同类工作。

从更广泛的产业视角看，规模化形式化能力未来将向更多硬核领域渗透，包括芯片设计、航空航天、工业控制系统等高可靠场景的形式化验证，以及大模型生成代码、逻辑方案的标准化校验，成为AI可信性体系的核心基础工具之一。