AxiomMath 用 AI 智能体形式化验证 Stacks 项目

AxiomMath 宣布已形式化验证数学巨著 Stacks 项目，其 AI 智能体将约 7,654 页内容翻译成约 1,600 万行 Lean 代码，由证明助手逐行检查。这家估值 16 亿美元的初创公司让智能体并行自主取任务，并自研数学模型，填补代数几何形式化验证的大片空白。CEO Carina Hong 认为未来 AI 工作需要可复用的验证知识库以避免 AI slop，并公开向编码公司发出挑战。