AxiomMath 将 Stacks Project 形式化为 1600 万行 Lean 代码

估值 16 亿美元的 AxiomMath 宣布已正式验证 Stacks Project，用 AI 智能体把这部约 7654 页的数学文献翻译成约 1600 万行计算机可检查的 Lean 代码。团队为智能体设定松散层级、让它们并行自行认领任务，并自研擅长数学的模型。CEO Carina Hong 称此举意在为 AI 智能体提供可复用的验证基础，减少低质产出，并公开向编码公司发起同等规模形式化的挑战。