知识卡片：Claude用11天完成费马大定理端到端形式化证明

一句话结论：据腾讯研究院AI速递转述，Anthropic 公布 Claude 用 11 天完成了费马大定理的首个端到端、可由计算机完整检查的形式化证明——数十个 Claude Agent 并行协作，生成约 1300 万行 Lean 代码，规模超过核心库 Mathlib 五倍。

事件概述 / 研究问题：

• 根据材料，Anthropic 公布的成果是：Claude 用 11 天完成费马大定理的端到端形式化证明。
• 所谓“端到端”和“可由计算机完整检查”，指证明被写成 Lean 形式化代码，而不是只生成自然语言证明。
• 本次事件展示的问题是：AI Agent 能否把费马大定理这类极高难度的数学定理拆解、协作并写成机器可验证的形式化证明。

方法 / 产品要点：

• 多 Agent 协作：数十个 Claude Agent 并行工作。
• 任务拆解：团队搭建 Prove2Me 平台，把证明拆成有向无环图（DAG），供各个 Agent 认领。
• 形式化工具：使用 Lean，材料称生成的 Lean 代码约 1300 万行，超过核心库 Mathlib 五倍。
• 基础性：材料称证明仅使用 Lean 三条最基础公理；具体含义和是否引入额外公理，待核实。
• 发起者：按材料称，项目发起者为清华姚班毕业、现任哥大助理教授的 Anthropic 研究员彭天翼；职位关系细节待核实。

主要结果 / 产业意义：

• 10 亿级工作量：项目消耗约 60 亿输出 Token。
• 可验证定理数量：产出约 30300 个可验证定理，其中 29500 个进入最终证明。
• 若 Anthropic 的说法属实，这意味着 AI Agent 不只是辅助写代码或做短任务，还能参与超大规模、长周期、结果可被机器严格验证的数学研究工程。
• 相比自然语言推理，这种形式化证明的优势是结果可以被 Lean 工具独立检查，不能靠模型“编造”蒙混过关。

为什么重要 / 与既有脉络的关系：

• 已有相关卡片主要涉及具身智能体、编码智能体吞吐和 UI 交互型 AI Agent；本条增量不在“执行操作”，而在“多 Agent 协作完成数学定理的端到端形式化证明”。
• 其特别之处是任务被拆成有向无环图供 Agent 认领，并且产出规模庞大：约 1300 万行 Lean 代码、约 3 万个可验证定理。
• 这个案例如果获得同行验证，可能为“AI 科研助手”提供新范式：模型生成“人不容易验证的长证明”，但机器可以逐行检查。

局限与不确定性：

• 原始材料是腾讯研究院AI速递的聚合摘要，不是 Anthropic 官方论文或官方公告全文，材料中也未给出 Anthropic 原始链接，待核实。
• “首个端到端形式化证明”的具体定义和比较范围，待核实。
• “约 1300 万行 Lean 代码”如何计数、是否包含自动生成或中间证明代码，待核实。
• 具体 Claude 模型版本、训练/推理总成本、是否公开发布代码库，均未在材料中说明，待核实。
• 项目结论尚未显示经过独立第三方复核。

可用于图书/PPT/简报的角度：

• 用“费马大定理 + AI Agent + 形式化证明”作为 AI 科研能力的案例。
• 用“60 亿 Token、11 天、1300 万行 Lean、Mathlib 五倍”做规模对比图。
• 用“Prove2Me 把证明拆成有向无环图”展示多 Agent 协作架构。
• 可延伸讨论：当 AI 生成的证明太长，超出了人的阅读审查能力时，“机器可验证”是否成为新的可信标准。

原始材料：

• 标题：腾讯研究院AI速递 20260907
• 相关条目：四、Claude用11天完成费马大定理端到端形式化证明
• 来源 URL：https://m.sohu.com/a/1072671882_455313?scm=10001.325_13-325_13.0.0-0-0-0-0.5_1334&digest_item=4
• 英文标题（供检索）：Anthropic Says Claude Completes End-to-End Formal Proof of Fermat’s Last Theorem in 11 Days
• 英文关键词：Claude; Anthropic; multi-agent; Lean; formal proof; Fermat’s Last Theorem