生成摘要

AI 生成，仅供参考

Claude完成费马大定理形式化证明：1300万行代码改变数学研究

2026年9月4日，Anthropic宣布Claude完成了费马大定理的首个端到端机器检查形式化证明。Claude基本自主运行11天，生成约1300万行Lean代码并完成29500个中间定理证明，项目以Apache 2.0协议开放代码。这一成果被伦敦帝国理工学院教授Kevin Buzzard评价为“足够稳固，可供后续研究继续构建”，数学与AI的协作方式正迎来里程碑式变化。

什么是形式化证明：为什么这件事如此困难

形式化证明是用机器可验证的严格逻辑语言，把数学证明逐步拆解并录入计算机，由Lean等证明助手检查每一步推导是否成立。它不同于日常的“论文式证明”——后者依赖审稿人的专业判断，而形式化证明每一步都必须通过机器的确定性检验。费马大定理是数学史上最著名的难题之一，其原始证明横跨数论、代数几何等多个分支，长达数百页，把这样的证明完整形式化，过去被认为需要耗费数学家人工数十年的工作量。

Lean证明助手是什么？

Lean是一个交互式定理证明器，它要求用户以严格的逻辑规则构造证明，并自动检查每步推理的正确性。在本次项目中，Lean既是Claude的“工作台”，也是最终验证者：模型每写一段代码，检查器立即反馈是否正确，这种即时反馈是长链自动推理能够持续纠错的基础。

Claude如何完成这项任务：11天与1300万行代码

据Anthropic Research披露，Claude在费马大定理形式化项目中基本自主运行了11天，生成约1300万行Lean代码，并完成29500个中间定理的证明。项目采用图结构任务分解：把庞大证明拆成可并行处理的子任务，多个智能体协同构造与验证，Lean检查器为每一步提供确定性反馈。最终成果以Apache 2.0协议开放，任何人都可以复核与复用。

多智能体协作如何实现“并行证明”？

Anthropic研究员Tianyi Peng介绍，项目核心是让多个智能体并行工作：系统先把大型证明按依赖关系拆成任务图，不同智能体分别构造与验证不同子定理，Lean检查器作为统一裁判持续反馈。这种“任务图+验证器+可复用中间成果”的架构，让超长科研任务具备工程化执行的可能。

这项成果对数学研究意味着什么

伦敦帝国理工学院教授Kevin Buzzard评价称，该机器形式化成果足够稳固，可供后续研究继续构建。机器检查把超长证明拆成可验证的中间定理，大幅降低大型协作中隐藏错误的可能。这意味着AI可以承担繁重的形式化工程，把数学家从机械验证中解放出来，把精力放在发现结构与提出新猜想上。

AI会替代数学家吗？

不会。中国科学院数学与系统科学研究院学术委员会在相关座谈会上明确指出，人工智能能够提高效率和拓展知识边界，但无法真正替代数学家。AI擅长的是把已有证明“翻译”成机器可验证的形式，而提出新问题、构造新概念、判断研究方向，仍然依赖人的创造与洞察。业界正在同步推进“MATH FOR AI”与“AI FOR MATH”两个方向，让数学与AI互为底座。

对AI科学研究范式的启示

费马大定理形式化项目提供了一个可复制的范式：当任务可以被拆解、每一步可以被机器验证时，AI智能体就能在超长周期内自主推进。这套方法论不仅适用于数学，也可能迁移到代码验证、科学计算、法律条文核查等领域。它同时提醒我们，AI科研的价值不在于“取代专家”，而在于把专家的时间从机械劳动中释放出来，聚焦更高层的创造。

普通读者可以从哪里了解更多？

建议阅读Anthropic Research发布的官方技术报告，以及伦敦帝国理工学院Kevin Buzzard教授的公开评述；对Lean形式化方法感兴趣的读者，可从Lean官方文档与社区教程入门，体验“机器验证数学”的基本流程。

常见问题（FAQ）

Claude真的证明了费马大定理吗？

费马大定理本身早已被数学家证明；Claude完成的是该定理的首个端到端机器检查形式化证明，即用Lean证明助手逐行验证这一经典证明，确保每一步都可由机器核查。

这次形式化证明用了多长时间？

Claude基本自主运行11天，生成约1300万行Lean代码并完成29500个中间定理证明。

费马大定理形式化项目的代码开放吗？

开放。项目以Apache 2.0协议公开代码，研究社区可自由复核与复用。

这项技术未来能用在哪里？

除数学外，同类“机器可验证的自主长链推理”可用于代码验证、科学计算、安全审计等领域，为高可靠性任务提供新的工程路径。

延伸阅读：欢迎查看本站AI百科栏目了解更多AI科普内容，关注AI技术栏目获取前沿研究解读。