人工智能似乎每周都在攻克新的数学难题。上个月，仅OpenAI一家就发布了719篇声称解决了该领域部分最难问题的手稿。然而，即便是计算机检查也可能出错。在经历多年的AI生成低质内容泛滥后，人们难免会担心，数学领域是否也会步其后尘。
AxiomMath正押注数学能够避免这种命运，它的方式不是放慢脚步，而是建立在更坚实的基础之上。这家估值16亿美元的初创公司，希望打造一个经过验证的基础体系，让AI智能体能够依赖它来编写软件，并最终用于科学研究。
周三，该公司宣布已完成对Stacks Project的形式化验证，这是人类撰写过的规模最大的数学著作之一。数学家们通常对Stacks给予极高的评价——哥伦比亚大学数学家彼得·沃伊特曾表示，"没有什么能与之相提并论"，并将该项目比作20世纪重塑数学基础的著名"布尔巴基丛书"系列。
沃伊特在哥伦比亚大学的同事约翰·德·琼于2005年创立了Stacks Project，作为一个开源参考资料库。此后，数学家们不断为其贡献内容，从大学水平的代数一直构建到代数、几何和数论领域最前沿的思想。
该公司的AI智能体团队将这部约7654页的文献库，转化为约1600万行经过计算机检验的代码。
数学形式化是一种确保其底层结构严谨性的方法。数学家们用一种名为Lean的编程语言将证明重写为代码，再通过一个叫做证明助手的程序逐行检查代码。如果证明通过检查，数学家就可以确信其在逻辑上是站得住脚的。
工程师们运用同样的理念——形式化验证，来确认芯片设计的正确性，而法国的研究人员则用它来排查计算家庭福利的软件中存在的漏洞。
对于像Stacks Project这样的文献库而言，逐一检验定理只是工作的一部分。Stacks中的定理和定义彼此相互关联，每一条都建立在前面结果的基础之上。就像一棵家族树一样，Stacks中的许多成果都能追溯到此前的内容。
这种紧密的关联性，最初让Axiom团队对项目能否成功心存疑虑。团队必须在大约1600万行Lean代码中，保持每一处关联完整无损。
"生活中，规模庞大的事物和精细脆弱的事物往往难以兼容，"Axiom首席执行官卡琳娜·洪告诉TechCrunch。"[Stacks]是数学基础的成果集合。你需要[定理]保持一致，不能自相矛盾。你需要定义之间不产生冲突。"
这位25岁的首席执行官从斯坦福大学数学博士项目退学，于2025年3月创立了这家公司。今年3月，Axiom完成了由Menlo Ventures领投的2亿美元A轮融资。
"我们当初并不确定，'氛围编程'式的方法能否保留Stacks的精妙之处，"洪说道。
为完成这一项目，团队给予其智能体一个较为松散的结构，并让它们并行运作。Axiom技术团队成员阿什温·斯瓦米纳坦表示："在Stacks项目中，我们确实设定了一种层级结构……[但]这并非一个完全自上而下、规定每个智能体具体任务的体系。智能体会自行寻找任务，并识别出可以并行处理的工作内容。"
Axiom还自行训练了擅长数学的模型，洪表示，这种方法是大多数其他验证类初创公司所未曾采用的。起初，团队依靠内部一位Lean专家，向智能体传授人类的审美判断力。洪表示，随着时间推移，这些智能体已经学会了自主形成这种判断力。
这一成果填补了数学形式化领域最大的空白之一。斯瓦米纳坦说："纵观数学形式化已经完成的领域，你会发现一个巨大的空白地带，而这个空白恰恰覆盖了代数几何。"
斯瓦米纳坦表示，在此之前，希望用Lean检验代数几何新成果的研究人员几乎没有什么现成基础可以依托。"而现在，他们有了。"
Axiom认为，每一个经过验证的成果都将成为一块基石，使未来的证明能够依托已检验过的数学成果，而无需从零开始。加州大学洛杉矶分校数学家、菲尔兹奖得主陶哲轩，曾更为简洁地阐述过这一普遍规律："你拥有的形式化证明越多，你就能创造出更多的形式化证明。"
数学家并非Axiom唯一的目标受众。长期以来，开发者一直难以保证自己的代码不存在漏洞和安全隐患。随着AI智能体承担起越来越多的全球代码编写工作，这一问题正日益凸显。
Axiom押注的是，未来的软件将需要建立在经过验证的基础之上，就像Stacks现在所实现的那样。
"我们相信，数学是人们开始构建这些体系的起点领域，而且这种能力是可迁移的，"斯瓦米纳坦说。"智能体可以阅读我们的代码、理解它，并在此基础上构建新的基础设施。我们的Lean形式化成果，如今已成为智能体可以在其上进行构建的基底。"
Axiom的智能体构建Stacks的方式——并行工作、自主选择任务——在洪看来，正是未来AI工作模式的缩影。她认为，AI智能体需要一个构建精良、可复用的知识体系，才能避免生产出低质内容。
"你希望[智能体]拥有一个可复用的资料库，供它们在此基础上构建，并不断拓展前沿，"洪说。"如果你从一开始就以糟糕的工程选择'倾倒劣质内容'，那么之后它们想要拓展这一边界将会非常困难。"
洪对这种方法信心十足，甚至公开发出挑战："我公开向所有编程公司发起挑战，希望它们也能在这样的规模上开展形式化验证工作。"
