Axiom Math 用 AI 智能体形式化验证 Stacks 数学库
原标题：Axiom Math wants to keep AI slop out of mathematics
AI 摘要
Axiom Math 宣布已用 AI 智能体将人类最大数学文献库之一 Stacks Project（约 7654 页）形式化为约 1600 万行 Lean 代码，并通过证明助手逐行验证。这家估值 16 亿美元的初创公司由 25 岁的 Carina Hong 于 2025 年 3 月创立，今年 3 月完成 Menlo Ventures 领投的 2 亿美元 A 轮融资。该成果填补了代数几何领域形式化数学的空白，公司希望为 AI 智能体提供可复用的验证基础，以减少代码与科学产出中的低质内容。
正文节选
It feels like AI is cracking a new math problem every week. Last month, OpenAI alone released 719 manuscripts claiming solutions to some of the field’s hardest problems. Even the computer checks can slip. After years of AI slop, it’s fair to wonder whether math is next. AxiomMath is betting math can avoid that fate, not by slowing down, but by standing on firmer ground. The $1.6B startup wants to build a verified foundation that AI agents can rely on to write software and, eventually, do science