AI 破解数学难题的新闻越来越多：上个月仅 OpenAI 一家就发布了 719 篇声称解决某些最困难问题的手稿。计算机辅助检查也可能出错。在一堆 AI 垃圾内容之后，Axiom Math 押注数学可以避开这个命运，不是放慢速度，而是站在更稳的地基上。这家估值 16 亿美元的初创公司想为 AI agent 建立可验证的基础，让它们写软件，最终做科学。

Axiom Math 本周宣布，它已正式完成 Stacks Project 的形式化验证。这是人类写过的最庞大的数学体系之一。数学家很少给这样的评价：哥伦比亚数学家 Peter Woit 说“没有真正可比的东西”，拿它比作 20 世纪从根基重建数学的 Bourbaki 系列。Stacks 由 Woit 在哥伦比亚的同事 Johan de Jong 于 2005 年发起，是开源参考书。数学家们此后持续贡献，从大学代数一路建到代数、几何、数论中最前沿的概念。

Axiom 用一组 AI agent 把 Stacks 图书馆约 7,654 页内容转成约 1,600 万行经计算机检查的代码。核心机制是形式化数学：把证明改写成 Lean 编程语言，再用一个叫 proof assistant 的程序逐行检查。证明通过，就可以在逻辑上信任它。工程师把这套方法称为形式化验证，用来确认芯片设计；法国研究者也曾用它抓过计算家庭福利软件的 bug。

验证 Stacks 不只是逐个定理检查。Stacks 里的定理和定义互相连接，像家谱，许多结果都能追溯更早的结果。这种相互连接让 Axiom 一开始没把握。团队必须让约 1,600 万行 Lean 代码里每一条连接都保持完好。25 岁的 CEO Carina Hong 对 TechCrunch 说：“又大又精细的东西通常没法共存。Stacks 是数学基础的一系列结果，你希望定理一致、不矛盾，定义彼此不打架。”

Hong 从斯坦福数学博士项目退学，2025 年 3 月创立公司，并在 3 月完成由 Menlo Ventures 领投的 2 亿美元 A 轮融资。她说团队不确定“vibe coding”能不能保住 Stacks 的美感。为了完成项目，团队给 agent 一个较宽松的结构，让它们并行工作。Axiom 技术成员 Ashvin Swaminathan 说：“我们加了层级，但不是规定每个 agent 具体做什么的完整层级。agent 自己找任务，识别出可以并行推进的事情。”Axiom 还训练了自己的数学模型，Hong 说多数验证公司没这么做。最初靠公司内部一位 Lean 专家教 agent 人类意义上的“品味”，后来 agent 自己掌握了这种判断力。

结果填补了形式化数学最大的空白之一。Swaminathan 说，此前已经形式化的数学里有个巨大黑洞，覆盖代数几何；研究者想用 Lean 检查代数几何新工作，几乎没有什么可依托。“现在有了。”Axiom 认为每条被验证的结果都成为构建块，后续证明可以站在已检查的数学上。UCLA 数学家、菲尔兹奖得主陶哲轩概括得更简单：“形式化证明越多，能做出的形式化证明就越多。”

数学家不是 Axiom 唯一的目标读者。开发者一直在和代码 bug、安全漏洞斗争，AI agent 写得越多，问题越大。Axiom 押注未来软件会像 Stacks 一样，必须站在被验证的地基上。Swaminathan 说：“数学是我们开始建这些东西的领域，这是一项可迁移的技能。Agent 能读我们的代码、理解它、在上面建新基础设施。我们的 Lean 形式化现在是 agent 可以搭建的基板。”

Hong 预期未来很多 AI 工作会像这次一样：agent 并行、自选任务。她说 agent 需要一个可复用知识库，才能避免产出垃圾内容；如果一开始用糟糕的工程选择把垃圾丢进来，边界就很难扩大。她向所有写代码公司下战书：“我公开挑战所有 coding 公司，来做这个规模的形式化。”