Anthropic 以 Apache 2.0 协议开源了一份费马大定理在 Lean 4 里的完整机器检查证明，代码建在数学库 Mathlib 之上。仓库给出的形式化陈述是：对任意 n ≥ 3 和正整数 a、b、c，a^n + b^n ≠ c^n。这句话在 Lean 里被写成一条可以被内核逐步核对的定理，不留任何缺口。
规模是这份工作最直观的部分。仓库统计到 60475 个模块、29511 条定理、1450 个定义模块，导出检查覆盖了 1052234 条声明；生成的 HTML 文档约 390 MB，完整导出文件 37.8 GB。想在本地跑一遍，需要 300 GB 以上磁盘，峰值内存约 153 GB。
三道检查，都留了记录
仓库没有只给一句”编译通过”。第一道是 Lean 4.33.1 自己的内核完整编译，96 核机器耗时 5 小时 32 分。第二道用 leanprover 官方的 comparator 工具（v4.33.0）复核，跑了约 14 小时 46 分。第三道换成 Rust 写的独立内核 nanoda 0.4.13，16 线程约 30 分钟，输出 Your solution is okay!。
三道检查之外还有一条硬约束：全部模块里不出现 axiom、sorry、native_decide、unsafe、extern、implemented_by、partial def 和 #eval。这几个关键字在 Lean 社区里是公认的漏洞入口，sorry 直接代表”这里还没证”，native_decide 则把一部分判断交给未经内核核对的机器码。把它们全部排除，等于承认这份证明的可信度只押在 Lean 内核和检查工具身上——README 自己也是这么写的。
AI 写了多少，仓库没说
按 README 的说法，Lean 源码由”AI 智能体在人类撰写的开源 Lean 代码之上产出，由 Lean 充当裁判”。具体比例没有披露：哪些模块是人写的、哪些是模型生成后被内核挡回去重来的，公开材料里查不到拆分。
人类的底子也标得比较清楚。106 个依赖文件来自已有学术项目，主要是帝国理工 Kevin Buzzard 主持的 FLT 形式化工程和处理库默定理的 flt-regular，另有 23 个模块重新证明了 Mathlib 里的内容。
放在形式化数学这条线上看，量级的跳跃比较明显。四色定理 2005 年由 Georges Gonthier 在 Coq 里完成形式化，开普勒猜想的 Flyspeck 工程 2014 年宣布收工，两者都以人年计。Buzzard 那边启动 FLT 项目时给外界的预期同样是多年跨度。这份仓库把终点提前了多少，取决于人机分工的真实比例，而这恰好是目前唯一查不到的数字。
参考来源：Anthropic 公开仓库自述与验证记录、CocoLoop、Mathlib 项目、帝国理工 FLT 工程公开材料；模块数、定理数与三项检查耗时按仓库口径核对。