Article · AI translation
感觉人工智能每周都在破解一道新的数学难题。就在上个月，单是 OpenAI 就发布了 719 篇手稿，声称解决了该领域一些最棘手的问题。即使是计算机检验也可能出错。经历了多年人工智能生成的劣质内容之后，人们有理由担心数学是否会成为下一个受害者。
AxiomMath 押注数学能够避免这种命运，靠的不是放慢脚步，而是建立在更坚实的基础上。这家估值 16 亿美元的初创公司希望打造一个经过验证的基础，让人工智能智能体能够依靠它编写软件，并最终开展科学研究。
周三，该公司宣布已对 Stacks Project 进行了形式化验证。这是人类有史以来编写的规模最大的数学知识体系之一。数学家往往对 Stacks 评价极高——哥伦比亚大学数学家 Peter Woit 曾称“确实没有别的东西能与之相比”，并将该项目与“著名的布尔巴基丛书”相提并论；后者是一套在 20 世纪从基础出发重建数学体系的著作。
Woit 在哥伦比亚大学的同事 Johan de Jong 于 2005 年启动了 Stacks Project，将其作为开放源代码的参考资料。此后，数学家不断为其作出贡献，逐步扩充其成果，涵盖从大学水平的代数到代数、几何和数论领域最前沿的思想。
该公司的一批人工智能智能体将这套文献约 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 轮融资。
Hong 说：“我们当时不确定凭感觉编程能否保留 Stacks 的美感。”
为了完成这个项目，团队给智能体设定了一个宽松的结构，让它们并行工作。Axiom 技术团队成员 Ashvin Swaminathan 说：“对于 Stacks，我们设定了一个层级结构……[但]它并不是那种完整到规定每个智能体具体做什么的层级结构。智能体会自行寻找任务，并找出可以并行处理的工作。”
Axiom 还训练了自己的模型，使其擅长数学。Hong 说，大多数其他从事验证的初创公司并未采取这种做法。起初，团队依靠一名内部 Lean 专家来教智能体形成类似人类的鉴别力。Hong 说，随着时间推移，智能体已自行培养出这种鉴别力。
这一成果填补了形式化数学领域最大的空白之一。Swaminathan 说：“看看数学中已经完成形式化的内容，就会发现一个巨大的空洞。而这个空洞覆盖了代数几何。”
Swaminathan 说，在此之前，想用 Lean 检验代数几何领域新成果的研究人员几乎没有可依托的现有成果。“好吧，现在他们有了。”
Axiom认为，每一项经过验证的成果都会成为一块基石，使未来的证明能够依托已核验的数学成果，而不必从头开始。加州大学洛杉矶分校的数学家、菲尔兹奖得主陶哲轩更简洁地阐述了这一普遍道理：“形式化证明越多，你能做出的形式化证明就越多。”
数学家并非Axiom唯一的目标受众。长期以来，开发者一直难以保证自己的代码没有漏洞和安全隐患。随着AI智能体编写全球越来越多的代码，这个问题也日益突出。
Axiom押注，未来的软件需要建立在经过验证的基础之上，就像Stacks现在这样。
“我们认为，数学是开始构建这些东西的领域，而且这项技能可以迁移，”斯瓦米纳坦说。“智能体可以阅读我们的代码、理解它，并在此基础上构建新的基础设施。我们的Lean形式化成果如今已成为智能体可以据以构建的基础。”
Axiom的智能体以并行工作、自行选择任务的方式构建了Stacks；洪认为，未来AI的大部分工作也会以这种方式进行。她认为，AI智能体需要一套构建完善、可重复利用的知识体系，才能避免产出粗制滥造的内容。
“你希望〔智能体〕有一个可重复使用的库作为构建基础，并不断推进前沿，”洪说。“如果一开始就随意丢出粗制滥造的东西，做出糟糕的工程选择，那么它们就很难拓展这一边界。”
洪对这一方法充满信心，甚至公开发起挑战。“我公开挑战所有编程公司，来做这种规模的形式化工作。”