Axiom把7500页Stacks Project搬进Lean：代数几何基础成为可导入的机器校验库
核心概要
Axiom发布Stacks Project的Lean形式化版本，把这部约7500页、奠定现代代数几何基础的开放参考书变成单一机器校验库，规模约1600万行代码。此前代数几何缺少对应的Lean基础设施，一个新证明往往要先串起交换代数、概形、层、上同调与代数栈的长链定理。该库保留原文永久标签，使研究者与AI智能体可直接导入定义和定理，并在形式化过程中定位到若干需要补假设或修正的陈述。
深度剖析
现代代数几何的基础文献现在有了一个整体形式化、可被机器逐条校验的Lean库，研究者和AI智能体可以把其中的定义与定理直接导入新的形式证明。 此前代数几何难以走这条路：一个当代证明在进入核心论证前，常要引用横跨交换代数、概形、层、上同调和代数栈的一长串定理，数学内容存在于Stacks Project，对应的Lean基础设施却不存在。 这次发布覆盖Stacks Project的完整数学展开，规模约1600万行代码，发布方称其为迄今最大的集成式可复用形式化数学库。
库沿用原文的永久四字符标签，每个Lean声明都能回指数学家熟悉的规范文本，读者可在同一界面上并排查看原文页面与对应Lean代码。 单个Stacks标签常展开为多个形式定义与引理，其中一些是新定义的，另一些直接桥接到Mathlib中已有的声明，界面显式记录这些映射。 配套站点stacks.axiommath.ai提供原文与Lean代码的并排浏览和交互式依赖图，形式化本身作为独立开源项目由Axiom维护。
形式化过程还反过来检查了原文：系统在Stacks Project中标出数十条需要局部细化的陈述，包括缺失的假设、正特征下的边界情形，以及按所述一般性并不成立的断言。 失败的证明尝试没有被当作障碍丢开，智能体诊断出数学上的阻碍，并构造显式反例来确定原陈述在哪里失效。 对局部疏漏，智能体找出确切缺失的假设，并把修正后的定理与反例一起形式化；当一条错误的辅助引理在更深定理的证明中造成缺口时，智能体在文献中找到替代路线，使主结果在原假设下成立。
启示与展望
已展示的范围是Stacks Project完整数学展开的Lean形式化，以及原文与形式代码并排浏览、依赖图追踪和反例查看的配套界面；该形式化是Axiom维护的独立开源项目，与上游Stacks Project仓库分开。
原文提到，2026年10月21日de Jong请求暂不要向上游Stacks Project仓库直接提交AI生成的评论和拉取请求；原文修正以“数十条”陈述的计数给出，未逐条列出，也未说明这些修正是否已被上游采纳。