AxiomMath 宣布完成 Stacks Project 形式化验证

AxiomMath 宣布已对 Stacks Project 完成形式化验证，用 AI 智能体把约 7,654 页数学内容转成约 1,600 万行 Lean 代码。这家估值 16 亿美元的初创公司称，该成果填补了代数几何在 Lean 中缺乏可复用基础的空缺。CEO Carina Hong 表示，智能体需要可复用的知识库来避免产出低质内容，并公开挑战编程公司做同等规模的形式化。