650多人编写20年的数学“百科全书”，华人初创用AI将其转化为可验证代码

过去 20 年间，代数几何学者需要查证一条基础结论时，最常打开的是一个名为 Stacks Project 的网站，它收录了 2 万多个领域内的定义、引理和定理，堪称代数几何的“维基百科”。而最近，这个网站上的内容有了一份可供计算机逐步检验的副本。

完成这项工作的是 AI 数学公司 Axiom Math。这家 2025 年成立的公司此前已相继完成了素数间隔 246 定理的形式化，把张益唐 2013 年开启的素数间隔前沿结果完整搬进了交互式定理证明器 Lean（一种既能编写程序、也能检查数学证明的软件）；近日还宣布完成了有限单群分类定理（CFSG）的形式化，这原本是 100 多位数学家跨越几代人完成的巨型证明。

当地时间 11 月 4 日，Axiom 再次交出约 1,575 万行代码，虽然篇幅不及 CFSG 形式化的四千万余行代码，但特别之处在于，团队搭建起了一整套持续更新、相互关联的数学知识体系。

AI 形式化数学的重心正从攻克一座座单独的山峰，转向修建可供后来者通行的道路。

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

2005 年起，哥伦比亚大学（Columbia University）数学家约翰·德容（Johan de Jong）着手搭建 Stacks Project，计划从交换代数出发，经由概形和代数空间，一路写到代数栈理论的完整基础，为代数几何构建完整的定义框架。

项目按照开源软件的方式运作，任何人都可以提交修改，但所有内容都由约翰一人逐条审核合并。经过 20 年积累，该项目已发展到 116 章、7,600 余页，贡献者超过 650 人。

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

图 | 一条定理背后的逻辑链。（来源：Axiom Math）

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

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

Axiom 交付了什么？

不到两个月后，这份“代价高昂”的工作就有了结果。据 Axiom 项目页面的说明，这套名为 Stacks 的代码库建立在数学库 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 的仓库中。

（来源：Stacks Project Blog）

从登山到修路

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 辅助生成