Axiom Math 正式验证 Stacks Project 并构建 AI 智能体数学基础

Axiom Math 宣布已完成对 Stacks Project 的形式化验证，将其约 7,654 页内容转化为约 1,600 万行 Lean 代码，旨在为 AI 智能体提供可信赖的数学基础以编写软件及开展科学工作。该公司通过训练专用模型和并行 Agent 协作，解决了代数几何领域长期存在的形式化空白，确保定理间逻辑一致且无悖论。

技术细节显示，团队采用分层结构让 Agent 自主发现任务并行处理，同时保留约 1,600 万行代码中的全部连接关系；CEO Carina Hong 指出这是首次将如此大规模的数学库进行完整形式化，此前代数几何存在巨大“黑洞”。该成果不仅服务于数学家，更面向开发者，试图解决 AI 生成代码时的漏洞与安全问题。

事实层面，Axiom 于 2025 年 3 月获得 Menlo Ventures 领投的 2 亿美元 A 轮融资，公司成立于 2025 年 3 月，当前估值 16 亿美元。推断其商业模式可能从单纯的技术服务转向提供经过验证的数学基础设施订阅或 API。猜测未来其他编码公司可能跟进类似规模的形式化工作，但具体时间表未披露。