Axiom Math 用 AI 整理 7500 页数学资料，生成约 1600 万行代码

11 月 4 日，AI 数学研究公司 Axiom Math 发布 Stacks Project 的 Lean 形式化版本。Stacks Project 是一部开放的代数几何参考资料，约有 7500 页；Axiom 将其中可形式化的内容转成约 1600 万行 Lean 代码，并开放项目库和对照阅读页面。[1][2]

Lean 是一种用于编写和检查数学证明的工具。研究人员可以用它描述数学定义、定理和证明步骤，再由程序检查这些步骤在形式逻辑上是否成立。Axiom 整理出的代码建立在 Lean 社区维护的数学库 Mathlib 之上，可以作为后续形式化证明的基础。[1][2]

从数学参考书到可调用的代码

Stacks Project 由哥伦比亚大学数学家 Johan de Jong 于 2005 年发起，经过数百名数学研究者多年协作，逐渐成为现代代数几何的重要开放参考资料。[1]

Axiom 的工作，是把资料中的数学内容转写成 Lean 可以处理的形式。项目页面将原文和对应代码并排展示，并提供交互式依赖关系图，帮助读者查看定义、定理之间的关联。代码中的条目也保留了与 Stacks Project 原文相对应的标识，研究者可以沿着标识查找出处。[1]

这项工作为后续研究提供了一批可以直接调用的数学定义和定理。研究人员在编写新的 Lean 证明时，可以引用已有内容；AI 智能体也可以使用同一套资料继续处理证明任务。[1]

代码分为两个层级

Axiom 在代码仓库中将成果分为两部分：StacksCore 中的形式化内容经过人工审阅，并与 Stacks Project 原文核对；StacksFrontier 收录 AI 智能体编写的内容。[2]

根据对项目元数据的独立整理，约 97% 的形式化条目属于尚未经过人工审阅的 AI 编写部分。[3] Lean 可以检查代码中的证明步骤，人工审阅则要进一步核对：代码表述的数学命题，是否准确对应原文中的命题。

Axiom 以 Apache 2.0 许可证开放项目代码。研究者可以在项目网站查看原文与代码，也可以从代码仓库获取材料。[1][2]

参考文献

[1] AXIOM. The Stacks Project, formalized in Lean[EB/OL]. (2026-11-04)[2026-11-09].

[2] AXIOM MATH. AxiomMath/Stacks: A Lean formalization of the Stacks Project[EB/OL]. [2026-11-09].

[3] AI PROVED WHAT? The Stacks Project, all in Lean? Axiom’s AI formalization, mostly not yet human-reviewed[EB/OL]. [2026-11-09].