Axiom发布整个Stacks Project的Lean形式化成果，约1600万行代码由AI智能体集群完成

为何重要

现代代数几何此前几乎没有Lean基础设施，因为一个证明可能依赖交换代数、概形、层和上同调中的一长串结果。Axiom表示，该库保留了Stacks Project的永久标签，人类和AI智能体可以直接将其中的定义和定理导入新的证明。此前Axiom已于2026年10月27日发布有限单群分类的Lean形式化。接下来要看对照原文核查陈述的数学家是否认为其忠实，以及该库能否与Mathlib一同被采用。