物界前沿物界前沿 · 资讯情报卡（TechCrunch · 2026/11/6）
Axiom Math用AI形式化验证Stacks数学库
核心事实
- Axiom Math宣布已对Stacks Project完成形式化验证，该数学库约7654页。
- 公司AI代理将Stacks内容转写为约1600万行Lean代码。
- Stacks Project由Johan de Jong于2005年发起，为开源数学参考库。
- Axiom Math成立于2025年3月，此前完成2亿美元A轮融资。
- 公司自研数学专用模型，并让代理并行自主认领任务。
关键数据
16亿美元公司估值
约7654页Stacks页数
约1600万行Lean代码行数
2亿美元A轮融资
物界观察
形式化验证把数学证明变成机器可逐行检查的代码，这是对抗AI生成错误内容的一条硬路径。Axiom选择代数几何这块空白切入，若验证结果可复用，受益的不只是数学家，还有依赖AI写代码的开发者。值得关注的是其代理并行自组织的工作方式，这可能成为AI协作生产知识的新范式。