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

Fermat's Last Theorem: 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 以下是因为纯数学成果离产品落地还远，但作为一条技术进展，信息量和话题性都够。