Axiom Math 用 AI 智能体形式化验证 Stacks Project，防止数学被 AI 垃圾污染

Axiom Math 周三宣布，已正式验证 Stacks Project——这是人类写过的最大规模数学文献之一。该公司的 AI 智能体集群将这座约 7,654 页的数学库翻译成约 1,600 万行计算机可检查的 Lean 代码，填补了代数几何领域形式化数学的一大空白。 Stacks Project 由哥伦比亚大学数学家 Johan de Jong 于 2005 年作为开源参考项目发起，内容从大学水平的代数一直延伸到代数、几何与数论领域最前沿的成果。形式化验证的做法是把证明改写成 Lean 语言代码，再由证明助手逐行检查，确保逻辑严密。难点在于 Stacks 中的定理与定义彼此关联、层层递进，团队必须在约 1,600 万行 Lean 代码中保持每一处连接完整。 Axiom 的做法是给智能体一个宽松的层级结构，让它们并行运行、自行发现可并行的任务，同时训练自家模型提升数学能力。CEO Carina Hong 表示，团队最初依靠内部 Lean 专家向智能体传授人类的品味，随着时间推移智能体已能自行掌握。她 25 岁，从斯坦福数学博士项目退学后于 2025 年 3 月创立公司，今年 3 月完成由 Menlo Ventures 领投的 2 亿美元 A 轮融资，公司估值 16 亿美元。 Axiom 的目标受众不止数学家。开发者长期难以保证代码没有漏洞和安全隐患，而随着 AI 智能体编写越来越多代码，这一问题会加剧。Axiom 认为未来的软件需要建立在经过验证的基础之上。UCLA 数学家、菲尔兹奖得主 Terence Tao 曾简明概括这一逻辑：形式化证明越多，能做出的形式化证明就越多。 Hong 认为，智能体并行工作、自行挑选任务的方式将是未来 AI 工作的重要形态，而它们需要一个构建良好、可复用的知识库来避免产出垃圾。她公开向所有编程公司发出挑战，希望它们参与这种规模的形式化工作。