品玩11月6日讯，据 TechCrunch 报道，估值16亿美元的AI初创公司Axiom Math近日宣布，已完成对数学领域重要开源参考书Stacks Project的完整形式化验证，将其约7654页内容转化为约1600万行经Lean证明助手逐行校验的代码。

该项目由多智能体并行协作完成，在保留原书高度互联结构的同时，填补了代数几何领域形式化数学库的空白。Axiom将成果分为经人工核验的StacksCore和待审阅的StacksFrontier两层，所有证明均由Lean内核检查，外部贡献者可逐步将前沿层内容移入核心层。

创始人Carina Hong表示，该库旨在为AI智能体提供可复用的知识底座，避免大规模代码生成中的低质输出问题，并开放挑战所有编程公司在同等规模上开展形式化工作。