Claude 11 天形式化费马大定理：1300 万行 Lean 证明了什么？

Claude 没有发现费马大定理的新证明，而是把已有的人类证明路线完整翻译成 Lean 可逐步检查的形式化证明。真正的突破是工程规模与速度：数十个智能体在 11 天内生成约 1300 万行 Lean，并让证明检查器完成端到端验证。

要点速览

Anthropic 9 月 4 日公布首个完整、可由计算机检查的费马大定理形式化证明。
项目用了 11 天、约 60 亿输出 Token，生成约 30300 个中间定理，最终证明使用其中约 29500 个。
这不是新数学路线，而是把 Darmon、Diamond 与 Taylor 对怀尔斯证明的简化阐述转换成机器可核验形式。
第一轮多智能体协作曾因丢失项目状态而失败；Prove2Me 的依赖图、搜索和任务协调是后来成功的关键。
Lean 能检查逻辑链是否成立，但代码规模、可读性、维护成本和进入 Mathlib 的人工评审仍是现实瓶颈。

“证明了”与“形式化了”有什么区别

费马大定理说明，当整数 n 大于 2 时，不存在满足 aⁿ+bⁿ=cⁿ 的正整数 a、b、c。Andrew Wiles 在 1990 年代完成数学证明，后与 Richard Taylor 修补审查中发现的缺口。今天的难题不是再次判断定理真假，而是把人类论文中省略的“显然步骤”全部展开，让证明助手能从公理开始逐行检查。

Anthropic 的官方研究说明把成果定义为 first complete computer-checked proof。官方也明确写道，创新点是 verification，而不是像开放数学问题那样产生新结论。New Scientist 的独立报道同样强调：Claude 是把现有证明变成可检查代码，不是替代怀尔斯重新发明证明。

因此，标题中的“Claude 证明费马大定理”如果不加解释，很容易误导。更准确的说法是“Claude 完成费马大定理端到端形式化，并通过 Lean 检查”。

1300 万行 Lean 是怎么产生的

人类数学论文可以引用常识、成熟文献和默认约定；Lean 需要每个对象、前提与推导都精确定义。项目最终生成约 1300 万行代码，规模超过 Mathlib 的五倍。数十个 Claude 智能体分别定义概念、证明中间引理，再逐层合并到最高目标。

关键并不是简单“多开几十个 Claude”。Anthropic 披露，早期智能体虽然快速产出局部结果，却逐渐失去全局项目状态，协作停止；这部分失败工作只贡献最终非模板代码的大约 7%。团队后来引入 Prove2Me，把定理关系组织成有向无环图，分离定理声明与证明文件，并为每个节点保存可搜索的自然语言描述。

The Next Web 对 Kevin Buzzard 复核的报道给出更重要的反面信息：Buzzard 在自己的环境中编译并检查了代码，也查看了可能利用 Lean 漏洞“作弊”的部分；他认为成果可信，但指出它没有增加新的数学知识，而且现阶段 1300 万行代码还不能直接进入 Mathlib 的人工评审流程。

为什么这个结果仍然重要

证明检查可以从稀缺手艺变成基础设施

大型证明的人工核验可能持续数月或数年。自动形式化若能稳定复现，就能把“是否漏了一步”交给机器，把专家时间留给概念、创造与解释。它也为后续研究提供可组合的定理库，让新结果建立在可验证依赖之上。

智能体系统的上限取决于协调框架

同一批模型在无组织协作时失败，在加入依赖图、共享状态、检索和任务分配后完成工作。这与“单个模型参数越大就一定能跑更久”的直觉不同。站内 OpenAI AI 研究实习生与智能体工时解析也讨论了类似问题：长期任务的价值取决于可审计工作流，而不只是一轮答案质量。

新瓶颈转移到阅读、维护和治理

机器能生成 1300 万行，并不表示社区能立即审完 1300 万行。代码是否简洁、能否模块化复用、依赖是否稳定、模型成本是否可承担，都会决定成果能否进入长期维护的知识库。

如何判断下一条“AI 证明了某定理”新闻

适用人群与前置条件

这套检查适合读者、研究团队、媒体和准备采购科研智能体的组织。前置条件是拿到定理陈述、代码仓库、证明助手版本和可复现构建说明，而不是只看实验室新闻稿。

先问是不是新定理。 区分发现新证明、补全已有证明、形式化已有证明和只通过题库测试。
确认裁判是谁。 Lean、Coq 等证明助手能给出机器检查结果；“模型自评正确”不算独立验证。
核对陈述等价。 确认机器验证的命题与公众讨论的命题完全一致，避免证明弱化版本。
检查公理与漏洞。 记录额外公理、sorry、不安全扩展和可能利用的编译器漏洞。
独立重建。 在干净环境固定版本、依赖和硬件，完整编译；只展示终端截图不是复现。
审计人类参与。 记录任务拆分、高层提示、修复次数、模型与 Token 成本，避免把人机协作写成完全自主。
评估可维护性。 查看模块化、文档、测试和上游社区是否愿意评审，而不只看行数。

常见误区与完成标准

“11 天超过 350 年”： 350 年对应发现数学证明，11 天对应形式化已有路线，两者任务不同。
“Lean 通过就没有任何风险”： Lean 检查给定形式系统中的逻辑，但仍需核对定理陈述、公理、工具链与实现漏洞。
“行数越多越强”： 巨量代码说明工程规模，也可能意味着重复和维护负担。
“多智能体自然会协作”： 本项目的第一轮失败恰恰说明共享状态和依赖管理不可缺少。

完成标准应包括：公开仓库可获取、固定环境能重建、定理陈述等价、无未关闭占位证明、额外公理透明、独立专家完成检查。对科研采购，还要补上成本、运行时长和失败记录。

想自己理解 Claude Code 的本地环境，可先阅读站内 Claude Code 安装与登录教程；比较不同助手的通用能力，则可参考 ChatGPT、Claude、Gemini 横评。

总结

Claude 的费马大定理成果不是“AI 独立发现了新数学”，而是大规模自动形式化跨过了一个重要门槛。最值得复制的不是 1300 万行这个数字，而是机器证明检查、多智能体分工、依赖图、共享状态和独立复核组成的完整工程链。它让证明更可验证，也把新的压力推向代码评审与长期维护。

FAQ

Claude 重新证明了费马大定理吗？

没有。它沿已有的人类证明路线完成形式化，让 Lean 可以逐步检查整个逻辑链。

Lean 通过是否等于数学结论绝对正确？

它对指定定理、所用公理和实现版本提供很强的机器验证，但仍需核对命题等价、额外公理和工具链漏洞。

为什么要写 1300 万行代码？

人类论文省略大量背景与显然步骤，Lean 要求把定义、依赖和每次推导全部明确表达。

人类在项目中做了什么？

人类提供高层方向、协作平台和复核；大量定义与中间证明由多个 Claude 智能体生成。

这份证明会直接进入 Mathlib 吗？

目前不能这样断言。独立报道指出，Mathlib 的人工评审与维护能力仍是主要瓶颈。

可复制的结构化数据

{
  "@context": "https://schema.org",
  "@type": "Article",
  "headline": "Claude 11 天形式化费马大定理：1300 万行 Lean 证明了什么？",
  "description": "解释 Claude 完成费马大定理机器验证的事实、技术路径、限制和复核清单。",
  "datePublished": "2026-09-08",
  "mainEntityOfPage": "https://next.ccgzs.xyz/blog/claude-fermat-last-theorem-lean-formalization-explained",
  "keywords": ["Claude费马大定理", "Lean形式化证明", "AI数学", "多智能体", "机器验证"]
}

{
  "@context": "https://schema.org",
  "@type": "FAQPage",
  "mainEntity": [
    {"@type":"Question","name":"Claude 重新证明了费马大定理吗？","acceptedAnswer":{"@type":"Answer","text":"没有。Claude 沿已有的人类证明路线完成了可由 Lean 检查的形式化。"}},
    {"@type":"Question","name":"Lean 通过是否等于数学结论绝对正确？","acceptedAnswer":{"@type":"Answer","text":"它提供很强的机器验证，但仍要核对定理陈述、公理和工具链版本。"}},
    {"@type":"Question","name":"为什么要写 1300 万行代码？","acceptedAnswer":{"@type":"Answer","text":"Lean 要求把人类论文省略的定义、依赖和推导步骤全部明确表达。"}},
    {"@type":"Question","name":"人类在项目中做了什么？","acceptedAnswer":{"@type":"Answer","text":"人类提供高层方向、协作平台和独立复核，多智能体负责大量定义与中间证明。"}},
    {"@type":"Question","name":"这份证明会直接进入 Mathlib 吗？","acceptedAnswer":{"@type":"Answer","text":"目前不能断言；人工评审、可读性和长期维护仍是瓶颈。"}}
  ]
}