Stacks：7500 页代数几何巨著译成 1600 万行 Lean，AI agent 干活，内核兜底

背景与现象：一份「史上最大」宣称与 94 颗星

2026 年 11 月 4 日，Axiom（axiommath.ai）发布署名博客，宣布完成整个 Stacks Project 的 Lean 形式化：约 1600 万行代码（官方自报口径，仓库过大，未做独立行数复核），号称「史上最大的集成、可复用形式化数学库」。对应仓库 AxiomMath/Stacks 采用 Apache-2.0 许可，工具链锁定 lean4 v4.34.0-rc2；按 2026 年 11 月 6 日抓取数据，仓库 94★，HN 条目仅 66▲、17 条评论。宣称的分量与回应的热度，形成了这期拆解的第一个观察点。为什么一份数学库的发布值得技术栏目拆解？因为它可能是目前规模最大的「AI 写代码、人定标准、机器验收」工程样本。

Stacks Project 本身是代数几何的地基：2005 年由哥伦比亚大学数学家 Johan de Jong 发起的开源参考书，约 7500 页，二十年间数百位数学人贡献，编辑原则是每定理带证明、假设显式、依赖可回溯到四位字符 tag，de Jong 自比「像维护 Linux 内核一样组织数学基础」。而现代代数几何的一个当代证明可能要跨交换代数、概形、层、上同调、代数栈的长定理链，Lean 此前恰好缺这一块基础设施。Axiom 的动机段说得很直白：AI 生成数学论证的速度已远超人工审查能力，形式验证因此成了必需品。

架构与技术原理：tag 映射、两层评审、多 agent 审计

第一层机制是永久对照。每个 Lean 声明都带 @[stacks TAG] 属性，链回 Stacks Project 原文的四位字符 tag；一个 tag 可对应多个声明，部分覆盖时由属性注释说明覆盖哪部分；Mathlib 已覆盖的 tag 则通过 add_to_stacks 注册到 Mathlib 声明上。声明同时标注其证明对应的 Grothendieck《EGA》《SGA》编号条目（如 @[ega] 属性带条目编号 IV 7.8.3），属性注释区分「整条/更一般/部分子句/特殊情形」四档。配套网站 stacks.axiommath.ai 提供原文与 Lean 代码并排浏览，外加交互式依赖图。

第二层是双层评审制度。仓库分 StacksCore 与 StacksFrontier 两个目录：Core 是人工审过、对照原文核过、达到 Mathlib 命名/一般性/风格标准的代码；Frontier 由 AI agent 所写，覆盖增长最快，进 Core 前最需要评审。README 说得明白：两层的唯一区别是「谁审过代码」，两者同样都经 Lean kernel 检查。

第三层是 agent 工程。Axiom 自述部署了「协调的 AI agent 集群」，并行翻译陈述、检索 Mathlib 现有抽象、构造证明、解决前置依赖，采用分层 agent 体系与严格协调协议（博客未给出协议细节）。声明忠实性靠三道机制保障：多 agent 审计、对原文的语义交叉检查，以及「每个定义引理必须与下游定理成功对接」的硬约束。

第四层是反例驱动的修正回路。形式化过程中发现了 Stacks 原文数十处需局部修正的陈述：缺失假设、正特征域的边缘情形、陈述过宽而不成立。agent 负责诊断数学障碍并构造显式反例；当假引理造成深层定理的证明缺口时，再从文献中找替代路径，在原假设下重建主定理。

关键数据：63k 模块、零 sorry、三条公理

以下数字均为官方自报或仓库自述口径，暂无第三方复核。

总规模自报约 1600 万行；README 自述约 63,000 个模块，并称「已形式化 Stacks Project 每个有可形式化内容的 tag」（README 自述口径），未形式化的 examples、exercises、remarks 留给社区当任务。

质量硬指标有三条：Lean kernel 检查每个证明；全库无 sorry、无 native_decide；只使用 propext、Classical.choice、Quot.sound 三条标准公理，任何人可用 #print axioms 命令验证。

构建成本是现实门槛：官方给的命令是 lake exe cache get && lake build，全量构建耗时耗内存都大；官方计划提供编译缓存服务，截至目前尚未上线。也就是说，这个 63k 模块的库对普通个人机器暂时不算友好。

社区数据：按 11 月 6 日抓取，仓库 94★；HN 条目（story 50380979，2026-11-05 发布）66▲、17 评论。评论区总量不大，质量却不低：既有对形式化路径的正面判断，也有对验证哲学的直接追问。作为参照，同组织 2026-10-27 发布过有限单群分类（CFSG）的形式化，Axiom 自己区分过两者：CFSG 围绕单个地标定理、组织松散；Stacks 是基础库，价值在数千个互锁的定义、构造、引理被反复复用，工程挑战本质不同。

影响与意义：把「声明忠实性」变成可审计的属性

第一是可用性。这不是纪念碑，是地基：数学家和 AI agent 可以 import Stacks 直接调用代数几何基础，用 #stacks_tags 与 #stacks_tags! 命令列出全部带 tag 声明。它补上的是现代代数几何在 Lean 生态里的空白，后续这个领域的形式化可以直接站上去，而不必从头再译一遍。对 agent 尤其如此：任务板把「哪些 examples 还没形式化」拆成可认领的工作项，README 明确欢迎社区评审 Frontier 代码移入 Core，等于给 AI 辅助的数学贡献预先铺好了轨道。

第二是形式化反哺数学的信号。数十处原文陈述被找出需要修正、agent 构造出显式反例，说明大规模形式化不只是翻译，还是一次对原文的自动审查。HN 有评论点出 Stacks Project 本身就近似「用自然语言写的 Lean」：每定理带证明、假设显式、依赖可回溯，所以高质量形式化并不意外；另一位评论者说 CFSG 发布后就料到会有人对 Stacks 动手。

第三是对数学之外 AI 工程的方法论启示（这是我的判断）。AI 批量生成代码时，最脆弱的环节往往不是证明能否通过，而是陈述是否忠实于原意：kernel 检查管得住前者，管不住「定理翻对了没有」。Axiom 给出的三件套——多 agent 审计、语义交叉检查、下游对接硬约束——本质是把「声明忠实性优先于证明正确性」做成了工程公理。这套思路可以直接迁移到任何 AI 翻译需求为代码的大规模审计场景。

争议与风险：上游拒收、文案批评与冷启动落差

最尖锐的边界在上游态度。2026 年 10 月 21 日，de Jong 在上游公告请求暂不向 Stacks Project 仓库直接提交 AI 生成的评论与 PR（Axiom 博客转述口径）。Axiom 表态尊重这条边界：形式化、反例、修正全部留在自己仓库，上游仍是 de Jong 与社区管理的活文本，供数学家按自己的节奏审阅取用。HN 有评论点出其中的尖锐处：原 Stacks Project 博客 10-21 的最新一篇恰好题为「No AI for now」，该评论者的代数几何朋友对 AI 数学进展感到沮丧。换句话说，这 1600 万行库目前只有独立项目的身份，尚未获得上游背书。

第二个争议关于文案。多位 HN 评论者批评发布博客是典型 AI slop：「This milestone begins with」这类隐喻混用，反而让人对结果信心不足。反驳的评论同样直接：有网友指认 Axiom 融资巨额（该评论者声称，未经独立核实），发布的是 AI 构建的大型 Lean 证明，AI 就写在人家域名里，何必挑剔文案里的 AI 腔。我的看法：文案批评不触及技术实质，但触及一个真问题：博客对「agent 集群」的协调协议没有开源文档，工程黑箱越不透明，文案腔调就越容易被放大审视（这是我的判断）。

第三是冷启动落差。「史上最大形式化数学库」的宣称，对上 94★ 与 17 条 HN 评论，热度明显不匹配。客观原因有：全量构建门槛高、缓存服务未上线、代数几何受众本来就窄。话题还出圈到了几何圈外：有评论者专门纠正跑题的讨论，说明此 Stacks 是代数几何里的「栈」，不是技术栈，这条误读本身印证了发布引发的关注已经越过专业边界。但 HN 也留下了审计哲学层面的疑问：假设的忠实性到底怎么验证？博客的多 agent 审计段其实是答案，只是提问的评论者自陈没读到。另一条评论更根本：即便证明全部正确，AI 时代数学的瓶颈仍是人的理解，不做题、不读证明的人不会因为库变大而获得理解。

结论与展望：能 import 的库才是真纪念碑

核心一句话：Axiom 把 7500 页代数几何巨著译成约 1600 万行 Lean 代码（官方自报），用三条标准公理、零 sorry、kernel 全检和 Core/Frontier 双层评审制度兜住正确性，但「上游拒收 AI 贡献」的身份边界仍未解决。

参与入口是现成的：import Stacks 即用，#stacks_tags 检索带 tag 声明；在 stacks.axiommath.ai/contributing 的任务板认领任务，GitHub issues 用 claim 标签防撞车；评审 Frontier 代码、推动其进 Core，是当下最被需要的贡献方式。后续值得盯三件事：编译缓存服务是否上线（决定 63k 模块能否被普通开发者用起来）、Axiom 是否公开 agent 协调协议细节（决定多 agent 审计能否被复现）、de Jong 的上游政策是否松动（决定这个库能否从独立项目汇入活文本）。

对普通开发者，即便不做代数几何，这个仓库也提供了一份可参照的样板：如何给 AI 生成的大规模代码库设计评审分层，如何把「忠实于原始需求」做成可检查的约束。我的结论一句话：Stacks 最有意思的不是 1600 万行这个数字，而是它把「AI 写的数学可信吗」拆成了两个可分别验证的问题：正确性交给 kernel，忠实性交给对照审计。前者它给出了硬保证，后者它给出了工程安排但没有协议级公开，这正是它当下最大的未决张力。

参考来源

• Axiom 官方博客（axiommath.ai，2026-11-04 发布，署名 Axiom；1600 万行、agent 集群、反例修正均为官方自报口径；全文存本地 stacks.txt）
• 仓库：github.com/AxiomMath/Stacks（94★ / Apache-2.0 / lean4 v4.34.0-rc2 / main 分支，2026-11-06 抓取快照；README 59 行已读全文；仓库过大未 clone，行数未实测）
• HN 条目：story 50380979（66▲ / 17 评论，2026-11-05 发布，2026-11-06 快照；评论池 hn-stacks-full.json 存证 11 条，正文全部转述，未直引）
• Stacks Project 上游背景与 de Jong 2026-10-21 公告：均为 Axiom 官方博客转述口径

署名：永亮