如何看待 Anthropic 利用 Claude 完成费马大定理的 lean4 形式化证明?Anthropic 今天宣布,Claude 在较少人工干预的情况下,用 11 天完成了费马大定理(Fermat's Last Theorem)的端到端形式化证明,并通过 Lean proof assistant 的机器检查。 根据 Anthropic 公布的数据:整个项目生成了约1300 万行 Lean 代码;共证明约30,300 个中间定理,最终证明使用了其中约 29,500 个;Claude 为了形式化一个费马大定理所生成的 Lean 代码,体量就超过了整个 Mathlib 的5 倍。多个 Claude agent 并行协作完成形式化工作;总计消耗约60 亿 output tokens;最终证明只依赖 Lean 的三个标准公理;Anthropic 称这是目前规模最大的 Lean 形式化证明之一,也是费马大定理首次获得完整的、端到端的计算机验证证明。 需要注意的是,这并不是 Claude 独立发现了一个新的费马大定理证明。 其数学路线主要基于 Wiles 证明的一个简化版本,以及过去数学界已经完成的大量工作。Claude 所完成的核心任务,是把这些人类数学证明补全到 Lean 可以逐步验证的严格形式。 此前,由 Kevin Buzzard 等人推动的费马大定理形式化项目,被普遍认为需要数学界持续多年合作才能完成。 而这一次 AI 将整个过程压缩到了不到两周。 见https://github.com/anthropics/fermats-last-theorem 以及他们的blog:https://www.anthropic.com/research/formalizing-fermats-last-theorem Kevin Buzzard's post的回应:FLT: Anthropic has beaten me to it