在人工智能频繁攻克数学难题的当下，一家名为 Axiom 的初创公司试图通过构建经过验证的基础设施，将 AI 引入更严谨的领域。该公司估值达 16 亿美元，其核心目标并非单纯加速计算，而是建立坚实的逻辑地基。
Axiom 近日宣布，已成功正式验证了“Stacks 项目”。这是迄今为止人类编写的最大规模数学项目之一。哥伦比亚大学数学家彼得·沃伊特（Peter Woit）对此评价称，“没有其他可比的东西”，并将该项目与 20 世纪重建数学基础的著名“布尔巴基丛书”相提并论。
Stacks 项目由哥伦比亚大学的 Johan de Jong 于 2005 年启动，最初作为开源参考库存在。多年来，全球数学家为其贡献了大量内容，涵盖从大学级代数结果到该领域最前沿的代数、几何和数论思想。
Axiom 的人工智能代理将该图书馆中 7,654 页的内容翻译成了约 1600 万行可由计算机检查的代码。这一过程涉及数学正规化，即使用 Lean 编程语言将证明重写为代码，并通过称为“证明助手”的程序逐行检查。若证明通过，数学家即可确信其逻辑严密性。类似的概念也用于芯片设计的正式验证以及法国研究人员捕捉福利计算软件中的错误。
对于 Stacks 这样的大型库而言，检查每个定理仅是工作的一部分。由于定理和定义相互关联，每一个都建立在前序基础之上，形成如同家族树般的依赖关系。这种复杂性使得 Axiom 团队起初对项目的成功持保留态度，因为必须确保跨越 1600 万行 Lean 代码的每一个连接完好无损。
Axiom 首席执行官卡琳娜·洪（Karina Hong）向 TechCrunch 表示：“生活中的大事和微妙事并不总是契合。Stacks 是数学结果的集合，也是数学的基础。我们需要确保定理之间的一致性而非矛盾，且定义之间不相互冲突。”
现年 25 岁的洪退出了斯坦福大学的数学博士课程，并于 2025 年 3 月成立了 Axiom。同月，该公司完成了由 Menlo Ventures 领投的 2 亿美元 A 轮融资。
“我们不确定‘振动编码’是否能够保护 Stacks 的美感，”洪说道。为了完成项目，团队赋予代理人松散的结构指引。尽管 Stacks 内部实行层次结构，但并非完全封闭。代理人需自行寻找任务，并确定可以并行处理的工作。
此外，Axiom 还训练了自己的模型以擅长数学，这与大多数其他验证初创公司的做法不同。团队依靠内部 Lean 专家教导代理人理解人类的“品味”，随着时间推移，据洪介绍，代理人逐渐形成了自己的判断标准。
这一成果填补了形式化数学中的一个巨大空白。斯瓦米纳森指出，此前试图用 Lean 检查代数几何新工作的研究人员几乎没有现成基础可用，而现在情况已改变。
未来的证明将能够依赖于经过检查的数学基础，而非从头开始。加州大学洛杉矶分校数学家、菲尔兹奖得主陶哲轩（Terence Tao）简化了这一逻辑：“你拥有的正式证明越多，就能做出越多的正式证明。”
Axiom 的目标受众不仅限于数学家。开发人员长期致力于保证代码无错误和安全漏洞，随着 AI 代理编写更多世界代码，这一问题日益严峻。斯瓦米纳森认为：“我们相信数学是你开始构建这些东西的领域，这是一种可转移的技能。代理人可以阅读我们的代码，理解它，并建立新的基础设施。我们的 Lean 形式化现在是代理商可以建立的基板。”
洪预计，未来 AI 的工作方式将类似于 Axiom 代理人构建 Stacks 的方式：并行工作并自主选择任务。她强调，AI 代理需要一个完善且可重复使用的知识库。“你希望代理人有一个可重复使用的图书馆，让他们继续前进。如果从一开始就做出糟糕的工程选择，它们很难跨越这个界限。”
洪对这种做法充满信心，并公开挑战所有编码公司在同等规模上进行形式化验证。
