Lobsters | 原文链接 | 2026-09-06 收录

用 Lean 形式化费马大定理：Claude 用 11 天写出 1300 万行机器可验证的证明

来源: anthropic.com — 2026-09-04

概述

Anthropic 公布了首个被计算机完整校验的费马大定理（FLT）证明。Claude 在 11 天里近乎自主地把它写进 Lean，共约 1300 万行代码、证明 29500 个中间定理，代码量超过数学库 Mathlib 五倍。难点在于把为人类读者写的证明补全到 Lean 能看懂每一步——社区此前预计要数年。这次成功的关键是 Prove2Me 协作平台：维护定理 DAG、把声明与证明分文件、加自然语言检索，让多个 Claude agent 能并行协作而不失忆。

核心要点

首个端到端、机器可校验的 FLT 证明，用 Lean 书写并经编译器与 comparator 验证
Claude 约 11 天产出 1300 万行 Lean、29500 个中间定理，代码量超 Mathlib 五倍
遵循 Darmon–Diamond–Taylor 对 Wiles 证明的简化表述，而非「现代证明」
关键转折是用 Prove2Me：以定理 DAG 缓解 agent 记忆退化、支持多 agent 并行
总计消耗约 60 亿输出 token；早期失败尝试约占最终非样板代码 7%

金句

This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics.

返回 Lobsters 首页