# Stacks Project 的 Lean 形式化

Axiom发布Stacks Project的Lean形式化版本，把这部约7500页、奠定现代代数几何基础的开放参考书变成单一机器校验库，规模约1600万行代码。此前代数几何缺少对应的Lean基础设施，一个新证明往往要先串起交换代数、概形、层、上同调与代数栈的长链定理。该库保留原文永久标签，使研究者与AI智能体可直接导入定义和定理，并在形式化过程中定位到若干需要补假设或修正的陈述。

Axiom发布Stacks Project的Lean形式化版本，把这部约7500页、奠定现代代数几何基础的开放参考书变成单一机器校验库，规模约1600万行代码。此前代数几何缺少对应的Lean基础设施，一个新证明往往要先串起交换代数、概形、层、上同调与代数栈的长链定理。该库保留原文永久标签，使研究者与AI智能体可直接导入定义和定理，并在形式化过程中定位到若干需要补假设或修正的陈述。