Axiom Math用AI形式化Stacks Project：1575万行代码进Lean库

二十年里，代数几何学者想核实一条基础结论，常去的是一个叫 Stacks Project 的站点。那里汇集了 2 万多个该领域的定义、引理和定理，被当作代数几何的“维基百科”。最近，站上的内容多了一份能让计算机逐步检验的副本。

做出这份副本的是 AI 数学公司 Axiom Math，2025 年成立。此前它已把素数间隔 246 定理形式化，将张益唐 2013 年开启的素数间隔前沿结果完整搬进 Lean——一款既能写程序、也能查数学证明的交互式定理证明器；近日又宣布完成有限单群分类定理（CFSG）的形式化，那是 100 多位数学家跨越几代人做出的巨型证明。

当地时间 11 月 4 日，Axiom 又交出约 1,575 万行代码。篇幅比不上 CFSG 形式化的四千万余行代码，但这次的不同在于，团队建起了一整套持续更新、彼此关联的数学知识体系。

AI 形式化数学的着力点，正从一座座孤立的山峰，转向修可供后来者通行的路。

一部“活着”的代数几何参考书

2005 年起，

项目照开源软件的路子运作，谁都能提交修改，但每一条内容都由约翰逐条审核、合并。20 年下来，项目已有 116 章、7,600 余页，贡献者超过 650 人。

Stacks Project 跟普通教科书最大的差别在组织方式：每个定义、引理和定理都带一个唯一且不变的 4 字符标签，数学家写论文时能直接引用；长证明在书中被拆成一串短小的中间引理，结论靠证明里的引用串成一张依赖网络，网站据此就能画出任意一条定理背后的逻辑链条。

约翰想让它成为一部“活的”书，始终处于修订和扩充中。这种高度结构化的写法，也让它在很早以前就被看作自动形式化的理想对象。2016 年就有研究者提出，用深度学习把 Stacks Project 翻译进定理证明器；2024 年 Lean 社区讨论这个话题时，有人称它是自动形式化的下一个大挑战。

到 2026 年 9 月，帝国理工学院（Imperial College London）数学家凯文·巴扎德（Kevin Buzzard）在个人博客回复读者评论时还说，形式化 Stacks Project 技术上大致可行，但代价高昂。

Axiom 交付了什么？

不到两个月，这份“代价高昂”的工作就有了结果。它建在 Mathlib 之上——那是 Lean 社区共同维护、所有代码都经人工审阅的开源数学形式化库——覆盖了 Stacks Project 中全部具备可形式化内容的标签。

按 Axiom 的说法，团队像管工程公司那样调度 AI 智能体：工作人员分派任务，一些智能体负责整体架构，一些编写核心定义，其余的逐条完成具体证明。形式化过程中，智能体还发现原书有数十处命题需要在局部加以修正，并在命题不成立的地方构造出了反例。Axiom 称，这是迄今规模最大、整合程度最高的可复用形式化数学库。

已收录进 Mathlib 的标签，和被判定不适用于 Lean 的标签，都单独做了标注；书中部分例子、习题和注释，则作为开放任务留给外部贡献者。网站上每个标签都能链接到对应的 Lean 代码和依赖项，读者可以顺着关系网络逐层追溯。

发布时，Axiom 还把这项工作当作对一种流行看法的回应：不少人觉得，大规模“氛围编程”（vibe coding，指主要靠向 AI 描述需求来生成代码的开发方式）只会产出难以维护的劣质代码。Axiom 称，这次 AI 生成的代码既优化了质量，又保留了原书高度互联的结构。

代码库的分层设计关系到后续维护。核心层（StacksCore）收录经人工核验、达到 Mathlib 代码规范的部分；前沿层（StacksFrontier）收录 AI 智能体编写、尚未经人工审查的部分。两层中的每条证明，都会由 Lean 内核检查。

Axiom 沿用了 Stacks Project 开放协作、集中审核的模式：外部贡献者可以认领前沿层的代码，审查后移入核心层；也能直接为核心层写新内容，但认领前要先交一份蓝图，写明精确的数学命题、拟证明的 Lean 命题、要调用的已有声明和证明大纲，经维护者批准后再动手。所有合并请求由 Axiom 团队中的 4 名数学家维护和审核，最终目标是把其中合理的部分并入 Mathlib。

早在 10 月 21 日，约翰就发布公告，要求暂时别把 AI 生成的评论和代码合并请求直接提交到 Stacks Project 的上游仓库。所以这套代码库与 Stacks Project 分开存放，相关内容目前都保存在 Axiom 的仓库中。

从登山到修路

Axiom 今年公布的三项形式化工作，目标一步步扩展。素数间隔项目验证的是 AI 能不能处理研究前沿的单个复杂证明；CFSG 的工程量大得多，约 15,000 页的证明被拆成 108 个里程碑，由数十个智能体分头完成。

这些只回答了 AI 能不能用来形式化证明，而且都有明确终点，最后一条定理通过检查，工作就算完；最新的形式化 Stacks Project 则是在验证 AI 产出的数学代码有没有更持久的生命力：AI 生成的代码不仅要经得起人类学者审阅，形式化工作也要从一次性交付变成持续维护。

AI 参与之后，大规模形式化也不再是 Axiom 一家的事。9 月，Anthropic 宣布其内部模型用 11 天写出超 1,340 万行代码，完成了费马大定理的 Lean 形式化，由凯文亲自编译并核对。国内外也出现了一批初创公司，想把 AI 与形式化验证结合成能落地的产品。

代码产出速度一下子提了上来，形式化社区开始琢磨：这些东西到底能给数学界留下什么？是 AI 公司之间的又一轮“军备竞赛”，还是真的会带来颠覆和变革？10 月 16 日，凯文和另外 6 位 Lean 社区核心成员联合发文，对“尽快把全部数学形式化”这种声音表示了忧虑。

文章的看法是，AI 产出的形式化成果如果没有人基于它去做数学工作，价值就相当有限。费马大定理本身已无争议，Anthropic 的这项工作很可能缺少持续价值；再说，AI 要是只能拿出一份粗糙的形式化，那还不如不做。

不过 Lean 社区也没有一味看衰。他们给出了几个方向，让 AI 形式化更可靠、更能复用：遵守 Mathlib 的设计规范，公开接受审查，避免重复劳动，还要和已有文献建立起可追溯的对应关系。

飞轮的另一头，卡在审查上。

一套可信、能调用的形式化库，对数学研究者和 AI 系统都直接有用。凯文 9 月就判断过，数千页文献既然能被智能体集群在十几天内端到端形式化，那前沿研究以后就能边做边验，论文审稿也会轻松不少。

对 AI 系统来说，经过内核验证、结构完整的数学库就是可靠的推理素材。智能体可以在已经验证过的结论上搜索、组合、往外扩，不用每回都从头证一遍。

Axiom 发布时说过，希望 AI 智能体去发现、使用这套库，并接着往里扩充。公司今年 3 月完成 2 亿美元 A 轮融资时，也把“可验证 AI”列为主要方向，从数学出发，延伸到代码、密码学和量化金融。库越完整，智能体能调用的结论就越多；产出的新代码又反过来充实库，循环就这样自我加速。

问题在于，眼下这个循环的速度主要受人工审查拖累。凯文在个人博客里提过，Mathlib 后台一直堆着大量未合并的代码请求，很多都在排队等人工审阅。他还判断，Mathlib 不接受 AI 审阅，所以就算 Stacks Project 被完整形式化，短期内也进不了 Mathlib。

已经有项目在试着用 AI 分担审查压力。Lean 专注研究组织（Lean FRO）和 Mathlib 计划（Mathlib Initiative）孵化了 Tau Ceti 项目，代码全部由 AI 编写，再交给其他 AI 按统一标准做对抗式审查，规则由数学家和形式化专家事先定好。该项目代码量已达约 300 万行，比 Mathlib 略多。

但不管审查的是人还是 AI，Lean 内核只能保证每一步推导合规，判断不了代码里的命题有没有忠实表达原书的数学含义。拿 Axiom 这项工作来说，前沿层的代码要想真正被信任，还是得人工逐条对照。

9 月，凯文还提到另一层期望：一旦机器能把艰深文献自动形式化，不完整的论证便无处藏身。联名文章的作者们判断，不出三年，多数数学内容都能以可继续搭建的形式完成形式化。数学家或许会因此回过头，补上那些躲在“显然”“同理可得”背后的逻辑缺环。效率之外，这是他的另一份期待。

参考内容：

https://stacks.axiommath.ai/

https://x.com/axiommathai/status/2118028838517219335

https://fourweekmba.com/ai-axiom-puts-the-stacks-project-in-lean-2-100-lines-per-page/

https://stacks.math.columbia.edu/

https://news.columbia.edu/news/stacks-project-johan-dejong

https://www.unite.ai/axiom-math-releases-43-1m-line-lean-proof-of-group-classification/

https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/

https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/

运营/排版：何晨龙

注：封面由 AI 辅助生成