11月4日，成立不到两年的 Axiom 宣布完成了一件在数学界看来近乎不可能的事：把 Stacks Project 整个形式化了。这部由哥伦比亚大学数学家 Johan de Jong 在2005年发起、数百位数学家贡献了二十年的开源代数几何参考书，约7654页，被转成约1600万行 Lean 代码，每一行都交给证明助手逐条检查。公司称这是史上规模最大的集成式可复用的形式化数学库。更有意思的是过程中出现的副作用：形式化过程中发现原文有数十条陈述需要补充假设或处理正特征下的边界情形，团队为其中一部分构造了明确的反例。
形式化数学不是新概念，芯片设计验证用了很多年，做法是把证明改写成 Lean 这样的语言，再由证明助手逐行检查逻辑是否有漏洞。通过检查，就意味着这条证明在逻辑上站得住，不依赖审稿人的耐心。
过去几年，形式化在数论、组合、分析等领域推进得比较快，因为这些领域的定理链条相对短，社区也积累了可复用的基础库。代数几何是个例外。一个当代证明在进入核心论证之前，往往要引用交换代数、概形、层、上同调、代数栈的一长串结果，每一层又要往下追。想用 Lean 检查一个新结论，得先有整条链上的所有前置定义与定理，而这块基础设施长期是空白。
这个空白不是没人想填，而是填起来太贵。一部参考书里的定义彼此咬合，改动一处可能牵动上千处引用。用没有协调的 AI 做，产出的东西互相不兼容，拼不起来。Axiom 的判断是，问题一半在数学，一半在软件工程：要让上百万行可验证代码拼成一个整体，需要干净的抽象与稳定的接口。
团队的做法是部署一支协调的智能体集群，并行翻译、证明与整合数千条定理。组织结构上给的是一个松散的层级，不是自上而下把每个任务指派到具体智能体。技术团队成员 Ashvin Swaminathan 的说法是，智能体会自己寻找任务，识别出哪些部分可以并行处理。
这个细节值得展开。大规模形式化最难的不是单点产能，而是依赖顺序：某些定义必须先立起来，后面几百条定理才能动。让智能体自己认领任务，前提是它们能读懂依赖图，判断哪一块已经具备开工条件。
公司还做了一件多数同行没做的事：自己训练专精数学的模型。CEO Carina Hong 提到，多数验证类初创公司不走这条路，直接拿通用模型改。Axiom 起初靠内部的 Lean 专家教智能体什么叫人类的数学品味。到后来，她说智能体开始自己长出这种判断力。这段话听起来像宣传，但它指向一个真实的技术选择：形式化不只是逻辑正确，还要在可维护性上过关，否则库会长成一团无法扩展的补丁堆。
发布材料里最不寻常的一段，是关于原文错误的。团队称形式化过程中浮现出数十条需要局部细化的 Stacks 陈述，比如缺少某个假设，或者在正特征的情形下边界没有处理好，并且为其中一些构造了显式反例。
这件事的分量在于它反向证明了形式化的价值。过去人们把形式化理解成"给 AI 的产出做质检"，方向是防机器出错。这次的实际情况是，机器在检查一部由人类写了二十年的权威文献时，找出了人类笔下的疏漏。原因不复杂：一条定理在写作时可能默认了某个上下文，读者也默认了，但机器不接受默认，缺一个假设就过不去。
当然，这个结论要带着保留看。反例的细节没有逐条公开，数量只说"数十条"，具体是哪些陈述、属于什么性质的疏漏，公开材料里没有列表。这类工作最需要的恰恰是同行的复核，而复核需要时间。
一个容易被忽略的技术难点，是形式化到底有没有忠实于原文。Lean 的内核只保证这段代码在逻辑上自洽，它不知道这段代码对应的是不是书里那句话。如果翻译时把定理的意思理解偏了，机器照样会点头。公司自己也承认这一点，明确表示把忠实度看得比证明检查更重。
他们的做法是多层核对：多智能体互审、与源文本做语义交叉核对、检查下游接口是否满足要求、对基础定义与标志性定理做定向审计。为了让人能查，每个 Lean 声明都带一个永久标签，指回 Stacks 原文的对应位置；在专门做的网站上，可以并排看原文与代码，还能浏览交互式的依赖图。
这套机制的有效性取决于审计覆盖到什么程度。定向审计是抽样，抽样就有漏的可能，而基础定义一旦偏了，上层几千条定理都会跟着偏。规模越大，越要在最底层花时间。
Stacks Project 是一个活的文本，还在被人持续修改。形式化成果要跟它保持同步，理想状态是把修正回灌到上游。但事实是，de Jong 在10月21日提出，暂时请不要把 AI 生成的评论与合并请求提交到上游仓库。于是 Axiom 把工作放在自己的仓库里，发现的修正与反例也留在自己那边。
这条边界很值得记录。它说明社区对 AI 参与的接受是分层的：接受成果，暂时不接受流程。理由可以理解，一个开源文档的维护者要面对的是可追溯性与责任，如果每天涌入大量机器生成的改动，评审成本会压垮志愿维护者。把成果放在平行仓库，数学家可以自己决定什么时候、以什么方式吸收，这是一种成本更低的过渡安排。对做 AI 工具的公司，这也是一个提醒：技术方案再完整，也要给社区的节奏留出位置。
菲尔兹奖得主陶哲轩对这个方向的概括被反复引用：你拥有的形式化证明越多，你就能创造出更多的形式化证明。这句话描述的是复利效应，每一条被机器检查过的结论，都是后来者可以直接调用的积木。
Axiom 押的注比数学更大。他们的论点是，AI 智能体正在以远超人类审阅速度的节奏产出数学论证，如果没有机器可检查的地基，产出越多，噪音越多。同样的逻辑可以挪到软件上：当智能体写下的代码占比越来越高，"这段代码对不对"就成了无法靠人工评审回答的问题。
需要保持清醒的地方同样清楚。库的规模、"史上最大"这些说法都来自公司自己的发布，没有独立验证；智能体数量、算力成本、耗时、使用的模型，一项都没有披露；忠实度检查以自动流程为主，定向审计是抽样。真正的检验在接下来一年：有多少数学家在它上面做出新结果，以及库在持续修改下还能不能维持一致。