Stacks Project 是现代代数几何的基础百科全书，该领域研究代数方程与几何形状之间的关系。该项目由 Johan de Jong 于 2005 年发起，将数十年来分散的数学知识——涵盖交换代数、层和上同调——组织成一个统一的、自包含的参考资料。因为它为代数堆栈等复杂结构提供了核心构建块，它经常被比作数学领域的“Linux 内核”：一个巨大的开源库，其中每一个定理都明确链接到其底层的假设和依赖关系上。
这张图片展示了 Stacks Project 的巨大规模和层级结构，Axiom 正在将其正式化为机器校验的库。
这些人物代表了 Stacks Project 所组织的数学概念的历史传承。
随着人工智能开始以超过人类检查能力的 tốc度生成数学论证，形式化验证成为了关键的保障措施。Axiom 的发布解决了代数几何中的一个重大瓶颈：虽然许多现代证明现在正在被形式化，但它们往往依赖于长链的先决定理，而这些定理此前缺乏机器校验的基础设施。为了弥补这一差距，Axiom 将 Stacks Project 翻译成 Lean，这是一种形式化证明语言。这项工作涉及管理 1,600 万行代码，这一任务不仅需要孤立的脚本。为了维护一个定义在成千上万个连锁引理中保持兼容的连贯库，Axiom 部署了一个协调的 AI 智能体层级系统。这些智能体并行工作，负责翻译陈述、在 Mathlib 库中搜索现有抽象概念，并解决先决条件，同时确保整个代码库中的每个定义保持一致。
正式化过程本身也是数学完善的工具。在项目过程中，系统识别出原始 Stacks Project 中的数十个陈述需要局部修正，例如缺失的假设或特定数学特征中的边缘情况。智能体并没有将这些视为失败，而是诊断了底层的障碍，并构建了明确的反例，以证明原始陈述在何处不完整。这些解决方案允许团队修复数学，以便下游章节仍能正常运行。虽然这个 Lean 正式化版本是 Axiom 维护的独立开源项目，但它保留了 Stacks Project 原有的永久标签结构，允许研究人员在 stacks.axiommath.ai 上将非正式文本与机器校验的代码并排查看。这一里程碑为人类数学家和 AI 智能体探索代数几何及其相邻领域的新前沿提供了经过验证的起点。