Axiom 用 AI 智能体集群把整部 Stacks Project 形式化为 Lean：约 1600 万行，称史上最大的可复用形式化数学库

核心背景与行业痛点

当 AI 生成数学论证的速度远超人工核查能力，形式化验证就成了刚需。但现代代数几何一直很难形式化：一个当代证明往往要先调用交换代数、概形、层、上同调、代数叠等一长串前置定理，而 Lean 里缺乏对应的基础设施。Stacks Project 由哥伦比亚大学的 Johan de Jong 在 2005 年发起，是约 7500 页、带永久四字符标签的开源代数几何参考书。Axiom 这次把它整体形式化，并在 X 上称其为“大规模 vibecoding 不等于垃圾代码”的反例。

架构亮点与底层机制

据官方博客，Axiom 设计了分层的 AI 智能体系统：各智能体分工明确、遵守严格协调协议，沿依赖图并行翻译命题、在 Mathlib 中检索已有抽象、构造证明并补齐前置条件，同时保持定义、类型类接口和抽象在各章节间一致，避免不同智能体对同一对象写出互不兼容的定义。命题忠实度通过多智能体审计、与原文的语义交叉检查，以及“每个定义和引理都必须能被下游定理使用”的硬约束来保证。

权威 Benchmark 与实测跑分对比

这不是跑分类发布。官方给出的数字是约 1600 万行代码、约 7500 页原文，“史上最大的一体化可复用形式化数学库”为 Axiom 自述，尚无第三方评测。形式化过程中发现了原文数十处需局部修正的命题，智能体给出了反例，并在可能时通过文献中的替代路线保住主定理。

开发者实战落地与开箱指南

数学研究者和做定理证明智能体的开发者可以在 stacks.axiommath.ai 对照原文浏览 Lean 代码、查看反例和完整依赖图，并在自己的形式化证明中直接 import 相关定义和定理。代码在 Axiom 的 GitHub 组织下开源。需要注意，de Jong 已要求暂不向上游 Stacks Project 仓库直接提交 AI 生成的评论或 PR，Axiom 的修正只保存在自己的仓库里。