Axiom Math 用 AI 智能体形式化验证 Stacks Project

感觉AI每周都在破解一个新的数学难题。仅上个月，OpenAI一家就发布了719份手稿，声称解决了该领域一些最难的问题。就连计算机检查也可能出错。在经历了多年AI粗制滥造之后，人们有理由怀疑数学是否会是下一个。

AxiomMath押注数学能够避免这种命运——不是靠放慢速度，而是靠立足于更坚实的基础。这家估值16亿美元的初创公司希望构建一个经过验证的基础，让AI智能体能够依赖它来编写软件，并最终从事科学研究。

周三，该公司宣布已对Stacks Project完成形式化验证，这是人类有史以来写下的最大数学文献之一。数学家们对Stacks一向给予罕见的推崇——哥伦比亚大学数学家Peter Woit曾声称“没有真正可比的东西”，并将该项目比作“著名的布尔巴基丛书”，那套丛书在20世纪从基础重建了数学。

Woit的哥伦比亚同事Johan de Jong于2005年作为开源参考发起了Stacks Project。自那以后，数学家们不断为其贡献内容，从大学水平的代数一直构建到代数、几何和数论领域最先进的思想。

该公司的AI智能体集群将这座文库约7,654页的内容翻译成约1,600万行计算机可检验的代码。

将数学形式化是确保其底层结构可靠的一种方式。数学家把证明改写为一种名为Lean的编程语言中的代码，再由一个名为证明助手的程序逐行检查代码。如果证明通过，数学家就可以相信它在逻辑上是可靠的。

工程师们使用同样的理念——称为形式化验证——来确认他们的芯片设计能够正常工作，而法国的研究人员则用它来捕捉计算家庭福利的软件中的漏洞。

对于像Stacks Project这样的文库来说，检查每一条定理只是工作的一部分。Stacks中的定理和定义相互关联，每一个都建立在前面的内容之上。就像一棵家谱树，Stacks中的许多结果都可以追溯到它之前的结果。

这种相互关联性让Axiom起初不确定这个项目能否成功。团队必须在约1600万行Lean代码中保持每一处连接完好无损。

“生活中，庞大的事物和精细的事物就是无法兼得，”Axiom首席执行官Carina Hong对TechCrunch表示。“[Stacks]是一批数学成果的集合，是数学的基础。你希望[定理]彼此一致，而不是自相矛盾。你希望定义之间不要相互冲突。”

这位25岁的首席执行官从斯坦福大学数学博士项目退学，并于2025年3月创立了这家公司。今年3月，Axiom完成了由Menlo Ventures领投的2亿美元A轮融资。

“我们当时不确定氛围编程能否保住Stacks之美，”Hong说。

为了完成这个项目，团队给智能体设定了松散的结构，让它们并行运行。“用Stacks，我们强加了一种层级……[但]它并不是那种规定每个智能体在做什么的完整层级，”Axiom技术团队成员Ashvin Swaminathan说。“智能体在为自己寻找任务，并找出可以并行开展的工作。”

Axiom还训练自己的模型擅长数学，Hong说大多数其他验证初创公司都没有采取这种做法。起初，团队依靠其内部的一位Lean专家来教智能体人类的品味。Hong说，随着时间的推移，智能体已经自己学会了品味。

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

Swaminathan说，在此之前，想要用Lean检查代数几何新工作的研究人员几乎没有可依托的基础。“好吧，现在他们有了。”

Axiom认为，每一个经过验证的结果都会成为一个构建模块，因此未来的证明可以依托经过检查的数学，而不必从零开始。加州大学洛杉矶分校数学家、菲尔兹奖得主陶哲轩更简单地概括了这一普遍情况：“你拥有的形式化证明越多，你能做出的形式化证明就越多。”

数学家并不是Axiom唯一的目标受众。开发者长期以来一直难以保证他们的代码没有漏洞和安全缺陷。随着AI智能体编写世界上越来越多的代码，这个问题愈发严重。

Axiom正在押注，未来的软件需要建立在经过验证的基础之上，就像Stacks现在所做的那样。

“我们相信，数学是你开始构建这些东西的领域，而且它是一种可迁移的技能，”Swaminathan说。“智能体可以阅读我们的代码、理解它，并在其之上构建新的基础设施。我们的Lean形式化现在就是智能体可以构建其上的基底。”

Axiom的智能体构建Stacks的方式——并行工作并自行挑选任务——正是Hong预期AI未来大部分工作会发生的方式。她认为，AI智能体将需要一个构建良好、可复用的知识体系，以避免产出粗制滥造的内容。

“你希望[智能体]拥有一个可复用的库，让它们能够在其上构建并不断推进前沿，”Hong说。“如果你一开始就以糟糕的工程选择粗制滥造地堆砌，那么它们就很难拓展那个边界。”

Hong对这一方法足够有信心，以至于发出了一项挑战。“我公开挑战所有编程公司，在这个规模上开展形式化工作。”