# Anthropic 用 AI 把费马大定理完整写进了 Lean 证明助手，只用了 11 天

> 原标题：Fermat's Last Theorem: Anthropic has beaten me to it

- 来源：Hacker News 首页
- 发布时间：2026-09-04T21:00:02.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/54829
- 原文：https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/

## 摘要

Anthropic 用自家内部模型和 prove2.me 平台，把费马大定理的证明完整形式化到了 Lean 里。他们走的是 1995 年 Darmon–Diamond–Taylor 那版老路线，只对 p≥17 的情况成立，但配合之前别人已经形式化过的奇正则素数情况，正好把 Freek Wiedijk 那个“100 个形式化挑战”清单上最后一项也收掉了。...

## 推荐理由

Anthropic 把费马大定理的证明完整形式化到了 Lean 里，Wiedijk 那个挂了多年的 100 题清单就此清空。这事对形式化数学社区是个大节点，HKR 三条全中：有竞争故事、有技术细节、有社区震动。分数压在 85 以下是因为纯数学成果离产品落地还远，但作为一条技术进展，信息量和话题性都够。

## 锐评

这件事最值得看的是速度：Anthropic 用内部模型和 prove2.me 平台，11 天就把费马大定理的完整形式化证明跑出来了，而原作者 Kevin Buzzard 拿了 EPSRC 资助，原计划要干五年。但别急着喊“数学已死”。首先，这个证明走的是 1995 年 Darmon–Diamond–Taylor 那版老路线，只对 p≥17 成立，不是 Buzzard 正在做的现代证明。其次，代码量超过 1340 万行，编译时间是 Lean 数学库的将近 20 倍，在 96 核机器上跑都费劲，这更像一次蛮力工程验证，而不是人类能读的数学文档。Buzzard 自己也说，这没产出可探索的动态文档，也没给数学本身增加新理解。

真正的信号在自动形式化能力上。能把几千页文献端到端塞进证明助手，意味着以后论文审查可能被机器辅助，那些“专家都知道”的模糊引用会被无情揪出来。但正文没披露 Anthropic 用了多少算力、模型具体是什么、有没有人工介入修正，这些缺口让“11 天”这个数字得打个折。另外，证明只覆盖了老路线，现代证明里更精细的部分还没碰，别急着说这个领域被终结了。