AI把Stacks Project搬进Lean

Axiom Math 在 11 月 5 日宣布，其 AI Agent 已将代数几何知识库 Stacks Project 形式化到 Lean 中，并交由 Lean 内核逐步检查。对 AI 数学而言，这比再拿下一套竞赛题更重要：模型不只是给出一个看起来合理的答案，而是在尝试把人类积累数十年的数学知识，转换成机器能够审计和复用的基础设施。

这也是 Axiom Math 在短时间内第二次用超大规模形式化工程展示其 Agent 系统。就在 10 月底，该公司刚刚宣布用数十个 Agent 在 24 天内处理有限单群分类定理（CFSG），生成约 4310 万行 Lean 代码和 205 万个形式化声明；如今目标从一项“巨型定理”转向持续更新的开放数学知识库，难度不再只是证明有多长，而是如何管理定义、依赖、版本和语义一致性。

Stacks Project 不是一本普通教材

**Stacks Project 是一个以代数几何为核心、由数学家长期协作维护的开放数学知识库。**它由数学家 Johan de Jong 发起，内容覆盖交换代数、范畴论、拓扑、概形、代数空间、上同调等主题，并通过稳定的 Tag 标识定义、引理和定理，方便论文精确引用。

Stacks Project 的工程属性与传统数学专著明显不同。它不是出版后基本冻结的一本书，而是一个持续修订的项目：章节之间存在密集依赖，错误可以被提交和修复，新内容也会不断加入。对形式化系统来说，这意味着“完成 Stacks Project”必须绑定到一个明确的代码快照或提交版本，否则项目今天完成，明天上游增加内容后就可能再次不完整。

Stacks Project 的真正价值也不只是篇幅庞大。代数几何中的大量结果会被后续证明反复调用，如果这些定义和定理能够成为经过 Lean 内核检查的模块，未来的 AI 或数学家就不必每次从自然语言教材重新理解上下文，而可以直接在一套明确的依赖图上继续工作。

换句话说，竞赛题更像测试模型能否独立解开一道锁，而 Stacks Project 更像让 Agent 把一整座城市的道路、管线和建筑规范重新绘制成机器可检查的工程图。后者不够适合做排行榜，却更可能产生长期复利。

“在 Lean 中验证”到底验证了什么

**Lean 是一种交互式定理证明器和函数式编程语言，其小型内核会按照形式逻辑规则检查每一步证明。**Lean 不会因为一段论证写得像数学论文就接受它；定义的类型不匹配、前提缺失或推理步骤无法成立，都会导致编译失败。

**形式化验证是把数学对象、命题与证明翻译成形式语言，再由证明助手机械检查推导是否合法的过程。**论文中常见的“显然”“类似可得”和“省略常规计算”，在 Lean 里通常需要被展开，或者明确引用已经验证过的引理。

这套机制解决的是“推导是否从给定前提严格成立”，但不会自动解决“形式化命题是否准确表达了原文”。如果 Agent 把待证明命题悄悄改弱，或者额外加入了一个足以推出结论、却没有得到证明的假设，Lean 仍可能接受这段代码。

一个直观例子是：原任务要求证明一座桥能承受重型卡车，Agent 却把命题写成“假设桥梁足够坚固，那么卡车可以通过”。后一句在逻辑上完全正确，Lean 也可以验证，但它没有完成原来的工程任务。

因此，Axiom Math 此次成果至少包含三层不同含义，三者不能混为一谈：

1. 语法与类型层通过： Lean 可以解析代码，类型检查没有失败。
2. 形式逻辑层通过： 定理确实由声明的公理、定义和前提推出。
3. 数学语义层对齐： Lean 中的定理与 Stacks Project 原始条目表达的是同一个数学结论。

前两层主要由 Lean 内核保证，第三层仍需要数学家、形式化专家和项目维护者审查。Axiom Math 的贡献，是把过去无法规模化检查的问题推到了第三层，而不是让人工审查彻底消失。

AI Agent 做的不是一次长对话

**AI Agent 是能够调用工具、读取环境反馈并反复修正行动的模型系统。**在 Lean 场景中，Agent 会读取目标和上下文，检索可用定理，生成证明片段，提交给编译器，再根据错误信息修改证明。

Axiom Math 的路线不是让单个大模型一口气吐出整座证明库。其 AxiomProver 强调多 Agent 协作：上层系统拆解任务，不同 Agent 分别处理定义翻译、定理检索、证明搜索、编译修复和依赖整理，再通过 Lean 编译环境把结果汇总。

这种流程与普通代码 Agent 很相似，但数学形式化的反馈更严格。代码测试只能覆盖预先设计的输入，而 Lean 内核检查的是证明项是否满足类型；一旦内核接受，至少可以确认推导没有在形式系统内部跳步。

Axiom 的底层基础设施 AXLE 则负责提供云端 Lean 4 编译、证明工具和并行执行环境。公开的 ICML 2026 AI for Math Workshop 资料显示，AXLE 已累计处理超过 5 亿次请求，也支撑了 AxiomProver 在 2025 年 Putnam 数学竞赛中取得 12/12 的成绩。

规模化基础设施在这个项目中不是附属品。Stacks Project 的条目之间存在大量交叉引用，一个上游定义发生变化，可能让下游成百上千个证明失效；如果没有稳定的构建环境、缓存、任务调度和依赖追踪，多 Agent 只会更快地产生冲突。

这次结果比竞赛跑分更有用

Axiom Math 此次工作的最大价值，是把 AI 数学从“一次性答案”推向“可复用知识资产”。竞赛题证明即便完全正确，通常也只解决单个问题；数学库中的定义、引理和自动化策略却可以成为后续数千个证明的基础。

| 维度 | 数学竞赛解题 | 自然语言长证明 | Stacks Project 形式化 | |---|---|---|---| | 主要目标 | 得到单题答案 | 给出人类可读论证 | 建立机器可检查知识库 | | 验证方式 | 标准答案或人工评分 | 同行评审 | Lean 内核检查加语义审查 | | 依赖规模 | 通常较小 | 可跨多篇论文 | 大量定义、章节和交叉引用 | | 复用价值 | 较低 | 取决于后续引用 | 可直接成为后续形式化依赖 | | 主要风险 | 猜中答案、论证跳步 | 隐含假设、引用错误 | 命题错译、依赖污染、版本漂移 | | 适合衡量的能力 | 局部推理 | 长程数学论证 | 工程调度、检索、证明与维护 |

这次项目也比 10 月的 CFSG 形式化更接近“数学软件工程”。CFSG 有相对明确的最终定理和既有证明路线，而 Stacks Project 是不断变化的知识库；前者更像完成一次超大型构建，后者更像接手一个长期维护的软件仓库。

| Axiom Math 项目 | 有限单群分类定理形式化 | Stacks Project 形式化 | |---|---|---| | 对象 | 一项跨越数百篇论文的巨型定理 | 持续更新的代数几何知识库 | | 已披露规模 | 约 4310 万行、205 万个声明 | 当前参考材料未给出可交叉核验的统一规模数字 | | 已披露周期 | 24 天 | 当前参考材料未给出完整工期 | | 核心挑战 | 超长证明拆解和依赖汇总 | 定义一致性、跨章节依赖和版本维护 | | 长期用途 | 审计与复用群论结果 | 为代数几何形式化提供基础库 |

值得注意的是，Axiom Math 此前公布的 4310 万行代码不能直接等同于 4310 万行高质量人类代码。形式化证明经常包含展开后的中间步骤和机器生成结构，行数更多代表工程规模，而不是证明“聪明程度”；真正重要的指标应是覆盖了哪些定理、使用了哪些公理、是否存在占位符，以及第三方能否从干净环境重新构建。

现在还不能只看发布稿下结论

Axiom Math 的宣布值得重视，但“已经形式化验证整个 Stacks Project”仍需要可复现材料支撑。数学形式化的可信度不应来自公司品牌或模型口碑，而应来自代码、构建过程和 Lean 内核。

一个足够完整的交付至少应公开以下信息：

• 对应 Stacks Project 的具体提交版本或快照；
• Lean 4、Mathlib 及其他依赖的精确版本；
• 定义、引理和定理的覆盖清单，以及原始 Tag 到 Lean 声明的映射；
• 是否存在 sorry、自定义不透明公理或未验证占位内容；
• 从空白环境完整构建所需的时间、算力与失败率；
• 自动生成内容与人工修订内容的比例；
• 数学家对高风险定义和关键定理所做的抽样或逐项审查。

其中最关键的不是代码总行数，而是“信任边界”。如果证明依赖未经解释的额外公理，或者大量关键结论仅以假设形式导入，那么仓库可以通过编译，却没有提供外界想象中的完整保证。

第三方复现也比发布当天的演示更重要。一个形式化仓库只有在外部研究者能够锁定依赖、重新构建、检查公理并追踪原始条目时，才真正从企业展示变成公共数学基础设施。

AI 数学正在从生成答案转向治理知识

Axiom Math 对行业争议给出了一条相对务实的路线。生成式模型不断产出自然语言证明，已经让数学界面临新的审核负担；如果这些结果无法验证，模型越强，研究者需要清理的内容反而可能越多。

形式化系统不能消除错误，但能把错误变得更容易定位。自然语言论文里的漏洞可能藏在一句“显然”中，Lean 项目中的问题则通常会落到某个缺失引理、错误类型、额外公理或不匹配的声明上，审计对象更具体。

这也解释了为什么 Stacks Project 是一个比刷榜更好的目标。它有清晰的章节结构、长期维护的标识系统和丰富的依赖关系，既适合 Agent 拆解，也能检验系统是否具备超长周期的工程能力。

不过，机器可检查不等于人类可理解。未来完全可能出现一种局面：Lean 确认证明正确，但证明项巨大、路线反直觉，没有数学家能够快速解释其中的核心思想。这样的结果可以用于依赖验证，却未必能直接推动数学理解。

Axiom Math 真正需要证明的，也因此不再是“AI 能不能写出足够多的 Lean 代码”。更难的问题是：这些代码能否被数学共同体维护、解释、复现和继续使用。

如果此次成果能够经受外部审计，它可能成为 AI for Math 的一个分水岭。模型公司的竞争重点将从解出多少道题，转向谁能构建更可靠的形式化知识库、谁能让 Agent 在严格反馈环境中长期工作，以及谁能把机器生成的证明变成数学家愿意依赖的公共设施。

参考来源

• Stacks Project GitHub 仓库：Stacks Project 的公开源文件、版本记录和协作维护入口。
• Lean 4 GitHub 仓库：Lean 4 语言、编译器与定理证明内核的官方开源仓库。
• Mathlib4 GitHub 仓库：Lean 社区数学库，可用于理解形式化证明的依赖与构建方式。
• Axiom Math 此前形式化有限单群分类定理的中文梳理：介绍 AxiomProver 的多 Agent 工作方式、4310 万行 Lean 代码及相关争议。