#AI
Anthropic 开源费马大定理机器证明
Anthropic 以 Apache 2.0 协议开源了费马大定理在 Lean 4 里的完整机器检查证明，代码建在 Mathlib 之上。这是 Freek Wiedijk 形式化 100 挑战清单中最后一个被攻克的定理，收尾了这份跨度约 20 年的基准榜单。
规模很直观：60475 个模块、29511 条定理，Claude 在 11 天内主要自主完成，写下约 1300 万行 Lean。仓库禁止了 axiom、sorry、native_decide 等已知漏洞关键字，并记录了三道独立内核检查全部通过，最终仅依赖三条公理。
💡 为什么值得看Claude 11 天完成费马大定理机器证明，终结 20 年形式化挑战。
查证
来源档案
CocoLoop
聚合媒体（中文 AI/数学新闻站）,汇总转载了 Anthropic 官方博客、官方技术论文 PDF、帝国理工 Kevin Buzzard 的博客等多源材料
事件本身为 Anthropic 官方一手发布，Buzzard 独立复现核验「checks out」,可信度高；但 e1 本体是二手聚合，具体数字应以官方仓库 README 与官方博客为准，尤其是「AI 撰写比例」这一官方未披露的缺口，任何媒体都补不上。
延伸阅读
这是全篇唯一查不到的关键数字：Buzzard 的 FLT 工程本按多年跨度立项，Claude 11 天完成到底多大程度是 AI 真自主、多大程度站在人类已有 106 个依赖文档上，决定了这条新闻在「AI 数学」这条线上的真实含金量。