感觉人工智能几乎每周都在攻克一个新的数学难题。上个月，仅 OpenAI 一家就发布了 719 篇手稿，声称解决了该领域一些最难的问题。即便是计算机检查也可能出错。在经历多年 AI 垃圾内容之后，人们不禁会问，数学会不会成为下一个受影响的领域。

AxiomMath 押注数学可以避开这种命运，方法不是放慢速度，而是建立更坚实的基础。这家估值 16 亿美元的初创公司希望打造一个经过验证的基础层，让 AI 代理能够依赖它来编写软件，并最终从事科学研究。

周三，该公司宣布已正式验证 Stacks Project，这是人类写下的最大数学成果之一。数学家们通常对 Stacks 评价极高。哥伦比亚大学数学家 Peter Woit 曾称它“几乎没有别的东西能与之相比”，并把该项目比作“著名的 Bourbaki 丛书”——那套在 20 世纪从基础重建数学的系列著作。

Woit 的哥伦比亚同事 Johan de Jong 于 2005 年启动了 Stacks Project，作为一个开源参考资料。此后，数学家们一直为其贡献内容，从大学水平的代数一路扩展到代数、几何和数论等领域最前沿的思想。

该公司的 AI 代理群把这套约 7,654 页的资料库翻译成了大约 1,600 万行可由计算机检查的代码。

形式化数学的目的，是确保其底层结构是可靠的。数学家会用一种名为 Lean 的编程语言把证明重写成代码，再由一个叫作 proof assistant 的程序逐行检查这些代码。如果证明通过，数学家就可以相信它在逻辑上是成立的。

工程师也用同样的思路，也就是形式化验证，来确认芯片设计是否可行；法国的研究人员则用它发现了计算家庭补助的软件漏洞。

对于像 Stacks Project 这样的资料库来说，逐个检查定理只是工作的一部分。Stacks 中的定理和定义彼此关联，每一个都建立在前面的内容之上。就像家谱一样，Stacks 里的许多结果都可以追溯到更早的结果。

这种相互关联性让 Axiom 一开始并不确定这个项目是否可行。团队必须在约 1,600 万行 Lean 代码中保持每一处连接都完整无缺。

Axiom 首席执行官 Carina Hong 告诉 TechCrunch：“体量大和精细这两件事在现实中通常并不相容。［Stacks］是一组构成数学基础的数学成果。你希望［定理］彼此一致，而不是像有悖论一样。你也希望这些定义之间不要互相冲突。”

这位 25 岁的 CEO 曾从斯坦福大学数学博士项目退学，并于 2025 年 3 月创办了这家公司。今年 3 月，Axiom 在 Menlo Ventures 领投下完成了 2 亿美元 A 轮融资。

Hong 说：“我们当时并不确定 vibe coding 是否能保留 Stacks 的美感。”

为了完成这个项目，团队给代理设定了一个宽松的结构，并让它们并行运行。Axiom 技术团队成员 Ashvin Swaminathan 说：“对于 Stacks，我们设定了一个层级……但并不是那种完全规定每个代理具体做什么的层级。代理会自己寻找任务，并识别出可以并行处理的事情。”

Axiom 还训练了自己的模型，让它们擅长数学。Hong 说，这种做法是大多数其他验证型初创公司没有采取的。起初，团队依赖一位内部 Lean 专家来教这些代理形成类似人类的判断标准。随着时间推移，Hong 说，这些代理已经自己学会了这种判断力。

这一成果填补了形式化数学中最大的空白之一。Swaminathan 说：“当你看已经被形式化的数学内容时，会发现有一个巨大的黑洞。而那个黑洞覆盖了代数几何。”

Swaminathan 说，直到现在，想用 Lean 检查代数几何新工作的研究人员几乎没有多少现成基础可用。“现在他们有了。”

Axiom 认为，每一个经过验证的结果都会成为一个积木块，未来的证明可以建立在已经检查过的数学之上，而不必从头开始。UCLA 数学家、菲尔兹奖得主 Terence Tao 用更简洁的话概括了这一点：“你拥有的形式化证明越多，你就能做出越多形式化证明。”

Axiom 的目标受众并不只有数学家。开发者长期以来都在努力确保自己的代码没有漏洞和安全隐患。随着 AI 代理编写越来越多的软件，这个问题只会变得更大。

Axiom 押注，未来的软件需要建立在经过验证的基础之上，就像如今的 Stacks 一样。

Swaminathan 说：“我们认为，数学是你开始构建这些东西的领域，而且这是一项可迁移的技能。代理可以阅读我们的代码，理解它，并在其上构建新的基础设施。我们用 Lean 做出的形式化，现在就是代理可以建立其上的底层基座。”

Axiom 代理构建 Stacks 的方式——并行工作、自己挑选任务——正是 Hong 预期未来许多 AI 工作的方式。她认为，AI 代理需要一个结构良好、可复用的知识库，才能避免产出垃圾内容。

Hong 说：“你希望［代理］拥有一个可复用的资料库，让它们能在上面继续构建并不断推进前沿。如果一开始就以糟糕的工程选择把垃圾塞进去，那么它们就很难再扩展那个边界。”

Hong 对这种方法非常有信心，甚至公开下了战书。她说：“我公开挑战所有编程公司，都来做这种规模的形式化工作。”