Axiom 把 Stacks Project 整部形式化进 Lean：约 7500 页代数几何参考书变成约 1600 万行机器验证代码，智能体还查出数十处需修正的命题

一部参考书，变成一个能直接 import 的库

数学 AI 公司 Axiom 11 月 4 日发布了 Stacks Project 的 Lean 4 形式化，代码以 Apache 2.0 许可放在 GitHub 的 AxiomMath/Stacks 仓库。Stacks Project 由哥伦比亚大学数学家 Johan de Jong 2005 年发起，是约 7500 页的开源代数几何参考书，每条结果都有固定的四字符标签（tag）。Axiom 称形式化版本约 1600 万行代码，基于 Lean v4.34.0-rc2 和 Mathlib，覆盖每个含可形式化内容的标签；例子、习题和注记还没做完，作为任务开放给贡献者。仓库说明写明没有 sorry，证明只依赖 Lean 的三条标准公理；全库约 6.3 万个模块，完整编译耗时长、占内存多。

这样做的直接好处是：形式化一个关于曲线族的新定理时，不必再从概形、上同调重新搭底座，可以直接引用现成的定义与定理。每个 Lean 声明用 @[stacks 标签] 挂回原书条目，网站 stacks.axiommath.ai 可以把原文和 Lean 代码并排对照。

AI 写的和人审过的分开放

Axiom 用分层协作的智能体群并行翻译命题、在 Mathlib 里查已有抽象、构造证明并统一各章接口。仓库把代码分成两层：StacksCore 是人工对照原书审核、达到 Mathlib 规范的部分；StacksFrontier 是智能体写成、尚待人工审核的部分。两层证明都经 Lean 内核检查，但「形式命题是否忠实于原文」主要靠多智能体审计和语义交叉核对，人工审计只覆盖基础定义和重要定理。

反过来查出原书的问题

Axiom 称过程中发现数十处需要局部修正的原命题：缺失假设、正特征下的边界情形、在所述一般性下不成立的论断。智能体为这些情形构造了反例；某个辅助引理有误、影响更深的定理时，则从文献里另找证明路线。de Jong 10 月 21 日曾请求暂不向上游提交 AI 生成的评论和 PR，Axiom 表示修正和反例只放在自己的仓库，供数学家自行取用。这些修正目前是 Axiom 单方披露，尚未见 Stacks Project 维护者逐条确认。