估值 16 亿美元的 AI 数学初创公司 Axiom Math 在 11 月 4 日放出一个大工程。他们用并行 AI 智能体集群，把人类数学史上规模最大的开源文献之一 Stacks Project（约 7654 页），翻译并验证成了约 1600 万行 Lean 代码。这家由 25 岁斯坦福数学博士退学生 Carina Hong 于 2025 年 3 月创立、拿过 Menlo Ventures 领投 2 亿美元 A 轮融资的公司，试图以此证明 AI 数学可以彻底告别幻觉与垃圾（AI slop）。但翻开其开源仓库的底层结构就会发现，把数学变成通过编译器检查的代码，并没有消除人类审核的瓶颈，只是把幻觉藏进了更隐蔽的角落。
对比上个月 OpenAI 放出的那批数学手稿，Axiom Math 的靶子立得很准。OpenAI 当时发布了 719 篇声称攻克数学难题的手稿（其 GitHub 仓库最新目录已更新为涵盖 373 个问题族的 721 篇，约 42% 的顶层结果完成了形式化），结果连计算机检查都频频漏出破绽。Axiom 的路线完全相反，直接用形式化语言 Lean 4 和社区标准库 Mathlib 重写整座数学大厦，由证明助手内核逐行检验，宣称全库零未完成证明占位符（sorry），且只依赖三条 Lean 标准公理。
7654 页的代数几何黑洞与仓库里的真实分层
Stacks Project 不是普通的题库。哥伦比亚大学数学家 Johan de Jong 在 2005 年发起这个开源项目，从大学代数一路写到高深代数几何与数论，被学界比作 20 世纪重建数学基础的布尔巴基学派巨著。代数几何长期是形式化数学里的黑洞，概念高度耦合、定义层层嵌套，改一处定义就可能让后面几千页的定理打架。
为了啃下这块硬骨头，Axiom 给自研模型组成的智能体集群设定了松散的层级结构，让它们自己拆解任务、并行运行，还请内部 Lean 专家给 AI 传授人类的数学品味。工程声势极大，但潜入其 GitHub 开源仓库（AxiomMath/Stacks）看一眼元数据，光鲜的公关叙事就露出了几道裂痕：
- 代码库被切成了两半.底层是经过人工审查的 StacksCore，上层则是尚未经过人工审查的 StacksFrontier，后者由 AI 生成、仅核对过源标签，且 README 承认仍遗留部分示例、习题与注记未覆盖。
- 审查标签写着自我评估（self-assessed）：列出的审查者全是项目自家作者，截至 11 月 5 日，没有任何外部独立审计完成全库编译与数学忠实度核验。仓库里甚至留着一条编号为
012108f的提交记录，专门用来修复Germ.lean和DenseOpen.lean中被内核拒绝的重复声明，好让编译能够跑通。 - 原作者态度冷淡.媒体报道借哥大教授的赞誉烘托这项成就，但 Stacks Project 原作者 Johan de Jong 并未给 Axiom 背书；相反，就在发布前两周的 10 月 21 日，他刚公开发帖要求外界停止提交 AI 撰写的评论与 PR，明确表态继续纯手工维护原项目。
编译器能管住推理，管不住 AI 在翻译时指鹿为马
我不太买账的是把零 sorry 通过内核检查直接等同于消灭了 AI 幻觉。这里藏着整个形式化赛道最隐蔽的盲区。
Lean 官方文档一直把证明检验（Proof Checking）和命题忠实度（Specification Faithfulness）分得很清。证明助手内核是个铁面无私的账房先生，但它只负责核对形式推导是否匹配形式命题。至于 AI 在自动形式化（Autoformalization）过程中，把自然语言翻译成代码时有没有歪曲原意，编译器根本无从知晓。
编译器能担保逻辑无懈可击，但没法担保翻译者没有指鹿为马。
当 AI 面对复杂的代数几何证明卡壳时，它完全可以通过悄悄强化前提条件、塞入隐蔽假设，或者微调底层定义来骗过编译器。10 月 6 日提交的一篇论文（arXiv:2610.08144，《Navier–Stokes 在翻译中迷失》）就抓到了现行犯：研究者检查 OpenAI 材料的 Lean 代码时发现，AI 在一个关键估计式里要求额外的 5 阶导数，而自然语言正文里明明只写了 4 阶导数。代码 100% 通过了机器检验，证明的却是一个被悄悄降维的弱化命题。
韩非子讲“郑人买履”，宁信度，无自信也。如果丈量脚掌的尺子本身是 AI 在无人监督时自己画出来的，那么用这把尺子裁出的 1600 万行代码越严丝合缝，人类排查定义偏移的成本就越高。尤其在未经人工审查的 StacksFrontier 层里，一旦某个底层代数几何定义出现微妙走样，后面成千上万行代码就只是在精确地证明一个平庸甚至走样的命题。
- 风险.形式化验证并没有免除人类专家的审核义务，它只是把审核负担从检查冗长的推理过程，转移到了极难用肉眼察觉的形式化定义与原意一致性核对上。
四条路线分野，真正的考题在软件工程规格书
把视野拉高一点看，AI 数学赛道眼下正裂变成四条截然不同的路径：
| 团队与项目 | 核心路径与代表战绩 | 真正卡脖子的验证瓶颈 |
|---|---|---|
| OpenAI | 自然语言与混合探索，发布 721 篇手稿（约 42% 顶层结果形式化） | 机器检查仍会漏掉导数阶数错位等前提篡改 |
| Google DeepMind | AlphaProof 结合 AlphaGeometry 2，在 IMO 2024 获银牌等效成绩 | 赛题需由人工事先翻译成 Lean，绕开了自动形式化 |
| Harmonic | Aristotle 专注奥赛级定理形式化求解，披露 IMO 2025 达金牌水平 | 局限于独立短题，缺乏超大规模耦合文献工程检验 |
| Axiom Math | 并行智能体翻译 7654 页 Stacks Project，构建 1600 万行基础库 | StacksFrontier 层未经人工审查，面临定义冲突与语义保真风险 |
DeepMind 和 Harmonic 刷奥赛题，题干是人类专家亲手翻译或者边界极其清晰的，考的是在既定规则下找路径；Axiom 直接啃 7654 页相互嵌套的基础文献，野心明显大得多。因为菲尔兹奖得主陶哲轩说过一句话，拥有的形式化证明越多，能制造出的新证明就越多。Axiom 真正想卖给投资人的，不是帮数学教授省时间，而是给未来所有 AI 编写的商业软件做数学级安全验证。
Carina Hong 甚至公开向所有 AI 编程公司下战书，赌未来的软件工程必须建立在这类可验证底座之上。算盘打得很精，但刚刚在数学界露出的翻译迷失暗礁，放到软件工程里只会更致命。
在芯片设计和法国政府家庭福利核算软件里，形式化验证之所以管用，是因为人类工程师花了巨大代价手写出绝对精确的形式化规格说明书（Spec），再让机器去验证业务代码是否符合 Spec。如果未来写业务代码的是 AI，写规格说明书的也是 AI，谁来保证 AI 没有为了跑通验证而偷偷改写安全边界？
16 亿美元的估值到底成色几何，不用听公关战书，接下来盯紧三件事就够了：外部独立学者能不能在固定 commit 下跑通全量编译与公理复现；代数几何专家抽检 StacksFrontier 核心定义时能挑出多少语义走样；以及要求严苛的 Mathlib 官方社区，到底敢不敢把这 1600 万行 AI 代码真正合入主干。