当 AI 每周都在宣称攻克新的数学难题，甚至出现计算机验证疏漏时，学界不禁担忧：数学是否会成为下一个 AI “垃圾”重灾区？估值 16 亿美元的初创公司 AxiomMath 选择了一条不同的路径：不降速，而是夯实基础。该公司旨在构建一套经严格验证的基础设施，供 AI 智能体信赖，用于编写软件乃至从事科学研究。
验证《Stacks 项目》：从7000页到1600万行代码
近日，AxiomMath 宣布已正式验证《Stacks 项目》（Stacks Project）。这是人类有史以来编写的规模最大的数学著作之一，由哥伦比亚大学数学家 Johan de Jong 于 2005 年发起，汇集了从基础代数到代数几何、数论等高深领域的成果。哥伦比亚大学数学家 Peter Woit 曾评价，该作品在重建数学基础方面的地位堪比著名的《布尔巴基丛书》。
AxiomMath 的 AI 智能体集群将这部约 7,654 页的巨著翻译成了约 1,600 万行由计算机检查的 Lean 代码。形式化数学通过“证明助手”逐行检查代码，确保逻辑严密性。这一技术此前已被工程师用于芯片设计验证，以及法国研究人员发现福利计算软件错误。
验证工作的难点在于《Stacks 项目》内部复杂的相互关联性。定理与定义环环相扣，如同家谱般追溯至早期成果。AxiomMath 团队需在千万行代码中保持所有连接的完整性，避免悖论与冲突。公司 CEO Carina Hong 指出：“生活中庞大与精细的事物往往难以共存，但我们需要确保定义间互不冲突，保持一致性。”
自研模型与并行智能体：填补代数几何空白
25 岁的 Hong 从斯坦福大学数学博士项目退学后，于 2025 年 3 月创立 AxiomMath，并于同月完成由 Menlo Ventures 领投的 2 亿美元 A 轮融资。为实现对《Stacks 项目》的验证，团队并未采用僵化的指令层级，而是赋予智能体松散结构，使其能自主寻找任务并并行处理。
与大多数验证类初创企业不同，AxiomMath 训练了自己的专用模型以擅长数学运算。初期，团队依靠内部 Lean 专家教导智能体具备人类的“品味”，随后智能体逐渐自行掌握了这一能力。Hong 坦言，团队起初并不确定这种“氛围编程”能否保留数学的美感，但最终结果证明了其可行性。
这一成果填补了形式化数学在代数几何领域的巨大空白。Axiom 技术团队成员 Ashvin Swaminathan 表示，此前希望用 Lean 检查代数几何新工作的研究人员缺乏可依托的基础，“现在，他们有了。”菲尔兹奖得主 Terence Tao 对此概括道：“你拥有的形式化证明越多，就能做出越多的形式化证明。”
构建 AI 时代的可信代码基座
AxiomMath 的野心不止于数学界。随着 AI 智能体编写越来越多的代码，软件漏洞与安全缺陷问题愈发严峻。公司认为，未来的软件将像现在的《Stacks 项目》一样，必须建立在经过验证的基础之上。
Swaminathan 指出，数学是构建这些事物的起点，且这是一项可迁移的技能。智能体可以阅读、理解现有的形式化代码，并在此基础上构建新的基础设施。Hong 强调，AI 智能体需要一个结构良好、可复用的知识库，以避免在初期因糟糕的工程选择而堆砌劣质内容，从而难以拓展边界。
基于对自身方法的信心，Hong 甚至向所有编码公司发出挑战：“要求你们在这个规模上开展形式化工作。”在 AxiomMath 看来，Lean 形式化已成为智能体可以依赖的基础层，这将决定 AI 未来工作的质量与高度。