7500 页代数几何被形式化：Stacks Project 全量进 Lean

📋 概述

Axiom 放出了整个 Stacks Project 的 Lean 形式化，代码约 1600 万行，是目前最大的可复用形式化数学库。Stacks Project 由哥伦比亚大学的 Johan de Jong 在 2005 年发起，二十年间数百位数学家贡献证明与例子，用永久四位标签组织，每个定理都带证明、每个假设都写明、每一步都指回依赖的标签——这套设计本身就接近形式化库的架构。把它整体搬进 Lean 的难点不只是数学，更是工程：不协调地让大量智能体并行生成，会得到一堆各自正确却难以组合的定义。Axiom 的做法是设计分层的智能体体系，在依赖图上并行翻译陈述、检索 Mathlib 里已有的抽象、构造证明、解决前置条件，并强制每个定义能与下游定理接口。过程中还发现了几十处需要局部修正的陈述，包括缺失假设与正特征下的边界情况，并给出了反例。