Axiom 完成 Stacks Project 全量 Lean 形式化

今天，Axiom 发布我们对整个 Stacks Project 的 Lean 形式化。Stacks Project 是一份约 7,500 页的开源参考书，为现代代数几何奠定了基础。此次形式化成果横跨约 1,600 万行代码，是迄今规模最大、可集成、可复用的形式化数学库。

借助这次发布，Stacks Project 的完整数学内容现在以一个经过机器检验的单一库的形式提供。研究者和 AI agent 都可以直接将其定义和定理导入新的形式化证明中，而永久的 Stacks 标签会把每一条 Lean 声明链接回数学家们早已熟悉的权威文本。

这一里程碑的起点是 Stacks Project 本身。它由哥伦比亚大学数学家 Johan de Jong 于 2005 年发起，二十年来在数百位数学家的不懈努力下不断成长，他们贡献了证明、示例和改进。我们的形式化工作同样建立在 Lean 和 Mathlib 社区的基础之上。能够形式化如此规模的语料，正是因为这些社区在我们的工作开始之前，早已花费多年构建了丰富的数学库，以及组织这些内容所需的抽象层。

为什么要形式化如此规模的基础参考书？随着 AI 系统开始以远超人工检查速度的节奏生成数学论证，形式化验证变得至关重要。在 Lean 基础设施成熟的领域，新成果往往在被发现后不久就能形式化。但迄今为止，现代代数几何要以这种方式处理要困难得多：一个当代证明在进入核心论证之前，可能就要调用横跨交换代数、概形、层、上同调和代数栈的一长串定理。这些数学内容存在于 Stacks Project 中，但相应的 Lean 基础设施并不存在。

弥合这一差距既是数学挑战，也是软件工程挑战。虽然缺乏协调的 AI 代码生成可以快速产出短小的孤立脚本，但要扩展到数百万行经过验证的数学内容，就需要清晰的抽象、稳定的接口，以及能在整个代码库中相互契合的组件。为实现这一点，我们部署了协同工作的 AI agent 集群，能够并行地翻译、证明和集成数千条定理。完整形式化 Stacks Project，为代数几何以及依赖其机器的众多邻近领域建立了一个新的起点。

代数几何的核心，是研究代数方程与其所描述的几何形状之间的相互作用。在实数上，方程 $x^2 + y^2 = 1$ 定义了一个圆；在有理数上，它的点对应毕达哥拉斯三元组，例如 $3^2 + 4^2 = 5^2$。在不同的数系中研究同一组方程，或在随参数空间变化的族中研究它们，把几何与数论和代数直接联系起来。这些思想还超出了纯数学：椭圆曲线保障着现代数字密码学，而有限域上的代数曲线则支撑着纠错码。现代代数几何为在所有这些情境下研究方程提供了一种共同语言。

锻造这种语言花了好几代人的时间。Emmy Noether 通过把焦点从单个方程转向环、模、理想等抽象结构，彻底改变了代数。正如恰当的软件抽象可以用一个可复用框架取代成千上万个专用例程，为正确的代数结构证明的定理可以同时适用于许多具体情境。一代人之后，Alexander Grothendieck 及其合作者引入了概形理论，在代数与几何之间建立了一部宏大的词典，使数学家能够在任意环上进行几何研究，并把算术和无穷小数据从一开始就内置其中。像 Éléments de géométrie algébrique（EGA）和 Séminaire de géométrie algébrique du Bois Marie（SGA）这样的巨著从零重建了这门学科的基础，为包括 Deligne 证明 Weil 猜想和 Wiles 证明费马大定理在内的里程碑式突破提供了机器。

然而随着这门学科不断扩展，其基础文献变得浩如烟海，散落在数千页艰深的专著和讨论班记录中，其中很多是用法语写成的。这门学科的许多实用知识还以不成文的民间传说形式，从导师传到学生。甚至定义一个代数栈——一种能够记住其所参数化对象内部对称性的几何空间——都需要一座令人生畏的前提高塔，横跨交换代数、拓扑、层和上同调。数学家们需要一份统一、自包含的参考书，把这些前提完整详细地写下来。

2005 年，de Jong 着手像软件工程师维护 Linux 内核这样的开源项目那样来组织这些基础。最初作为代数栈入门读物的内容，逐渐演变成一部活的、协作式的百科全书，包含数千个永久的四字符标签。Stacks Project 遵循严格的编辑原则：每条定理都带有证明，每个假设都被明确陈述，每一步都回溯到它所依赖的确切标签。通过这种方式，de Jong 及其合作者预见了形式化证明库的架构，表明当数学内容的组件拥有稳定的标识符和显式的依赖图时，数学会变得更容易验证和扩展。把 Stacks Project 翻译成 Lean，为这一由人类设计的架构带来了机器验证。

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）