Axiom 完成 Stacks Project 全部内容的 Lean 形式化

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

借助这一发布，Stacks Project 的完整数学展开内容 now 以一个经过机器校验的单一库的形式提供。研究人员和 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 及其合作者引入了概形理论，在代数与几何之间建立了一部宏大的词典，使数学家能够在任意环上进行几何研究，并将算术和无穷小数据从一开始就内置其中。诸如《代数几何原理》（EGA）和《Bois Marie 代数几何讨论班》（SGA）这样的巨著从头重建了该学科的基础，为包括 Deligne 证明 Weil 猜想和 Wiles 证明费马大定理在内的里程碑式突破提供了背后的机器。

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

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

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