Axiom 用 AI 将 Stacks Project 全部形式化为 1600 万行 Lean 代码
Axiom Math 于 11 月 5 日宣布完成对整个 Stacks Project 的形式化：约 1600 万行基于 Lean 的可验证代码，覆盖数百章、数万条数学结果，被视为对「AI 大规模生成代码必是 slop」这一流行论调的有力反击。
已确认
- 规模与内容：整个 Stacks Project 被形式化为 Lean 定义与证明，约 1600 万行代码，横跨数百章的数万条结果（@Scobleizer、@ChrSzegedy）。
- 工程基础：构建于 Mathlib 之上，所有已完成的证明均由 Lean kernel 自动验证；项目中每个带四字符标签的定义、引理、命题与定理都有对应的 Lean 形式化版本（@LinusEkenstam、@rohanpaulai）。
- 质量与结构：据发布信息，形式化保留了原书高度互联的依赖结构，并附带可视化的依赖图，代码质量经过优化（@Scobleizer、@LinusEkenstam）。
- 背景脉络：Stacks Project 原由 Johan de Jong 发起，是代数几何领域最大的开源教科书与参考著作，被多位作者称为现代数学（尤其是代数几何）的关键基础设施（@LucaAmb、@m5 转述的 Ken Ono 说法、@ChrSzegedy）。
- 数学界关注：数学家 Ken Ono 公开宣布该项目，并将其定位为 Axiom Math 继 CFSG（有限单群分类）形式化之后的又一步，目标是保存并验证人类已有的数学成果（@LucaAmb）。
为什么重要
- Stacks Project 属于数学中最深奥的领域之一，其完整形式化意味着大量现代代数几何成果首次获得机器级验证，兼具数学保存与验证价值。
- 该成果由 AI 在大规模、高互联结构下完成且通过 Lean kernel 检查，直接回击了「AI 大规模写代码必是垃圾」的质疑，成为 AI 编程能力讨论中的重要反例。
- 依赖图的可视化展示了如此庞大证明网络的互联结构，对后续形式化工程与 Lean 社区具有参考意义。
2026-11-05 ~ 2026-11-05 · 6 条相关
一手来源
- Axiom 发布 1600 万行 Stacks Project 形式化，反击大规模 AI 代码必烂论 — Scobleizer ·
- Stacks Project 代数几何全书被 Lean 形式化并可视化依赖图 — LinusEkenstam ·
- Stacks Project 启动 Lean 形式化:代数几何全书证明交由内核验证 — rohanpaul_ai ·
- 【源头】Axiom 发布 1600 万行 Stacks Project 形式化，反击大规模 AI 代码必烂论 — Scobleizer · 2026-11-05
- 【源头】Stacks Project 代数几何全书被 Lean 形式化并可视化依赖图 — LinusEkenstam · 2026-11-05
- Axiom Math 发布 STACKS，用 Lean 保存并验证人类已有数学成果 — LucaAmb · 2026-11-05
另有 3 条近重复转述:rohanpaul_ai · kimmonismus · ChrSzegedy