Axiom Math 用 AI 代理完成 Stacks Project 形式化验证

OmniTools 11月6日消息，Axiom Math 宣布，其 AI 代理已完成对 Stacks Project 的形式化验证。Stacks Project 由哥伦比亚大学数学家 Johan de Jong 于 2005 年发起，是开源数学参考库，覆盖代数、几何和数论等领域的成果。

Axiom Math 的 AI 代理将该项目约 7654 页内容转换为约 1600 万行经计算机检查的 Lean 代码。形式化验证通过 Lean 编程语言重写证明，并由证明助手逐行检查代码，以确认逻辑可靠性。公司称，Stacks Project 中定理和定义相互关联，团队需在约 1600 万行 Lean 代码中保持所有连接完整。

Axiom Math 由 25 岁的 Carina Hong 于 2025 年 3 月创立，她曾从斯坦福大学数学博士项目退学。该公司此前完成由 Menlo Ventures 领投的 2 亿美元 A 轮融资，估值 16 亿美元。其 AI 代理在项目中以并行方式运行，并自行寻找可处理的任务；公司还为数学任务训练了自有模型。

Axiom Math 表示，此次工作填补了代数几何领域形式化数学的一大空白，并认为经过验证的结果可作为后续证明和 AI 代理开发的基础。该公司还提出，未来 AI 编写的软件也需要建立在经过验证的基础之上。