11月6日，据techcrunch消息，估值达16亿美元的ai初创企业axiom math宣布，已成功完成对数学领域关键开源参考文献stacks project的全面形式化验证工作。该项目将原书约7654页的内容，精准转化为约1600万行代码，并全部通过lean定理证明助手进行逐行验证。
整个验证过程由多个AI智能体协同并行推进，在完整保留Stacks Project原有高度网络化知识结构的基础上，有效填补了代数几何方向在形式化数学库建设方面的长期空白。Axiom将此次成果划分为两个层级：经人工严格审核的StacksCore，以及尚待社区审阅的StacksFrontier；所有数学证明均经由Lean内核自动检查，外部开发者可依据规范，逐步将Frontier层中成熟内容迁移至Core层。
公司创始人Carina Hong指出，该形式化知识库的核心目标是为AI智能体构建一个高可信、可复用的基础知识底座，从而显著缓解当前大规模代码生成过程中普遍存在的低质量输出问题。同时，Axiom公开向全球编程公司发起挑战——鼓励各方在同等规模下开展形式化数学工程实践。
☞☞☞AI 智能聊天, 问答助手, AI 智能搜索, 多模态理解力帮你轻松跨越从0到1的创作门槛☜☜☜
