Axiom Math 完成对 Stacks 项目约 1600 万行 Lean 代码的形式化验证

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

AxiomMath 打赌数学可以避免这种命运，不是靠放慢速度，而是靠站在更坚实的基础之上。这家估值 16 亿美元的初创公司想要构建一个经过验证的基础，供 AI 智能体依靠来编写软件，并最终从事科学研究。

周三，该公司宣布已对 Stacks Project 完成形式化验证，这是人类撰写的规模最大的数学著作之一。数学家们对 Stacks 往往推崇备至——哥伦比亚大学数学家 Peter Woit 曾表示“几乎没有其他可与之相比的”，并将该项目比作“著名的布尔巴基丛书”，那套丛书在 20 世纪从基础开始重建了数学。

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

该公司的AI 智能体集群将这套约 7654 页的文献翻译成大约 1600 万行经计算机检查的代码。

数学形式化是确保其底层结构可靠的一种方法。数学家用一种名为 Lean 的编程语言将证明重写为代码，然后由一个称为证明助手（proof assistant）的程序逐行检查代码。如果证明通过，数学家就可以确信它在逻辑上是可靠的。

工程师们用同样的思路，即形式化验证，来确认他们的芯片设计可行，而法国的研究人员也用它来发现漏洞，对象是计算家庭福利的软件。

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

正是这种相互关联性让 Axiom 一开始不确定这个项目能否成功。团队必须在大约 1600 万行 Lean 代码中保持每一个关联完整无损。

“生活中，庞大的东西和脆弱精致的东西往往难以兼得，”Axiom CEO Carina Hong 告诉 TechCrunch。“[Stacks] 是一系列数学成果的集合，是数学的基石。你希望[这些定理]是一致的，而不是自相矛盾的。你希望这些定义之间互不冲突。”

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

“我们当时不确定凭感觉写代码（vibe coding）能否保留 Stacks 的精妙之处，”Hong 说。

为了完成这个项目，团队给它的智能体一个宽松的框架，让它们并行运行。“对于 Stacks，我们设定了一个层级结构……[但]它并不是那种规定每个智能体做什么的完全层级结构，”Axiom 技术团队成员 Ashvin Swaminathan 说。“智能体们会自己寻找任务，并确定它们可以并行处理的工作。”

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

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

Swaminathan 说，到目前为止，想用 Lean 来验证代数几何新工作的研究者几乎没有什么可依托的基础。“嗯，现在有了。”

Axiom 认为，每一个经过验证的结果都会成为一块基石，这样未来的证明可以依赖已验证的数学，而不必从零开始。加州大学洛杉矶分校的数学家、菲尔兹奖得主 Terence Tao 曾更简洁地陈述过这个普遍道理：“你拥有的形式化证明越多，你能做出的形式化证明就越多。”

数学家并不是 Axiom 唯一的目标受众。开发者们在保证代码没有漏洞和安全缺陷方面早已苦苦挣扎。随着 AI 智能体编写世界上越来越多的代码，这个问题还会不断加剧。 

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

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

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

“你希望【智能体】拥有一个可复用的库，让它们在其上构建并持续推动前沿，”Hong 说。“如果一开始就 slop 掉、做出了糟糕的工程选择，那么它们就很难扩展这个边界。”

Hong 对这种方法有足够的信心，甚至发起了挑战。“我公开挑战所有编程公司来做这种规模的形式化工作。”

当你通过我们文章中的链接购买时，我们可能会获得少量佣金。这不会影响我们的编辑独立性。