感觉AI每周都在破解一道新的数学难题。上个月，OpenAI发布了 719份手稿声称解决了该领域一些最棘手的问题。但即使是旨在确认这些结果的计算机检查也可能出现疏漏。 在经历了多年的AI低质内容后，人们不禁要问，数学是否会是下一个重灾区。
Axiom Math 押注数学可以避免这种命运，不是通过放慢脚步，而是通过建立在更坚实的基础上。这家估值16亿美元的公司希望构建一个经过验证的基础设施，让AI代理能够依赖它来编写软件，并最终进行科学研究。
周三，该公司宣布它已正式验证了《Stacks项目》，这是人类有史以来编写的最大规模的数学著作之一。数学家们通常对《Stacks》评价极高——哥伦比亚大学数学家Peter Woit曾声称“没有其他真正可与之相提并论的作品”，并将该项目与“著名的布尔巴基丛书”相提并论，后者是一套在20世纪从基础重建数学的系列著作。
Woit的哥伦比亚大学同事Johan de Jong启动了 Stacks项目 ，作为开源参考资料。自2005年以来，数学家们一直参与其中，从大学水平的代数结果出发，逐步构建出涵盖代数、几何和数论领域最前沿思想的成果。
公司的 AI智能体集群 将图书馆中约7,654页的内容翻译为约1,600万行经过计算机验证的代码。
形式化数学是一种确保其底层结构健全的方法。数学家将证明过程重写为一种名为Lean的编程语言中的代码，并由一个称为“证明助手”的程序逐行检查代码。如果证明通过，数学家就可以确信其在逻辑上是严谨的。
工程师使用相同的理念，即形式化验证，来 确认他们的芯片设计能够正常工作，而法国的研究人员则利用它来发现计算家庭福利的软件中的错误。
对于像Stacks Project这样的图书馆来说，检查每个定理只是工作的一部分。Stacks中的定理和定义相互关联，每一个都建立在前面的定理之上。就像家谱一样，Stacks中的许多结果都可以追溯到之前建立的定理。
这种相互关联性最初让Axiom对项目能否成功持怀疑态度。团队必须保持约1,600万行Lean代码中所有连接的完整性。
“生活中庞大与精微的事物往往难以共存，”Axiom首席执行官Carina Hong对TechCrunch表示。“[Stacks] 是一组数学成果的集合，构成了数学的基础。你希望[定理]保持一致，而不是像悖论那样自相矛盾。你希望定义之间不要互相冲突。”
这位25岁的首席执行官从斯坦福大学数学博士项目中退学并于2025年3月创立了该公司。同年3月，Axiom完成了由Menlo Ventures领投的2亿美元A轮融资。
“我们不确定‘氛围编码’（vibe coding）能否保留Stacks的美感，”Hong说。
为了完成这个项目，团队给其智能体提供了松散的结构，并让它们并行运行。“对于Stacks，我们施加了一种层级结构……但并非那种完全规定每个智能体具体做什么的严格层级，”Axiom技术团队成员Ashvin Swaminathan说。“智能体自行寻找任务，并识别出可以并行处理的工作。”
Axiom还训练了自己的模型以擅长数学运算，Hong表示这是大多数其他验证初创公司尚未采取的方法。起初，团队依靠内部的一位Lean专家来教导智能体一种人类的审美品味。Hong表示，随着时间的推移，智能体已经自行掌握了这种品味。
这一成果填补了形式化数学领域最大的空白之一。“当你审视已被形式化的数学内容时，会发现存在一个巨大的黑洞。而这个黑洞涵盖了代数几何领域，”Swaminathan说。
在此之前，希望用Lean检查代数几何新研究的研究人员几乎没有可依托的基础，Swaminathan说。“现在，他们有了。”
Axiom认为，每个经过验证的结果都成为一块基石，未来的证明可以依赖已检查过的数学知识，而不是从头开始。加州大学洛杉矶分校（UCLA）数学家、菲尔兹奖得主Terence Tao， 更简洁地阐述了这一普遍观点：：“你拥有的形式化证明越多，你就能做出的形式化证明就越多。”
数学家并非Axiom唯一的预期受众。开发人员一直在努力确保代码没有漏洞和安全缺陷。随着AI智能体编写越来越多的世界代码，这一问题日益严峻。
Axiom押注的是，未来的软件将需要建立在经过验证的基础之上，就像Stacks现在所做的那样。
“我们相信，数学是构建这些事物的起点，而且这是一项可迁移的技能，”Swaminathan说。“智能体可以读取我们的代码，理解它，并在此基础上构建新的基础设施。我们当前的Lean形式化工作已成为智能体可以依托的底层基础。”
Axiom的智能体以并行方式构建Stacks，并自主挑选任务，Hong认为这正是未来大部分AI工作方式的样子。她指出，AI智能体需要一个结构良好、可复用的知识库，以避免产生低质量的内容。
“你希望[智能体]拥有一个可复用的库，以便在其基础上构建并不断拓展边界，”Hong说。“如果一开始就因低质量输出而做出糟糕的工程选择，那么它们就很难再拓展这一边界。”
Hong对这种方法充满信心，甚至发出挑战：“我公开向所有编程公司发起挑战，要求它们在如此规模上开展形式化工作。”