Axiom Math用AI代理形式化验证Stacks项目

估值16亿美元的Axiom Math称其AI代理将约7654页的Stacks Project转译为约1600万行Lean代码，完成形式化验证，以应对AI生成证明泛滥、缺乏校验的问题。

• OpenAI内部模型产出722篇数学手稿2026-10-31
• HN讨论：数学家为何抛弃OpenAI2026-10-17
• Thomas Hales谈Lean定理证明器的可靠性与AI2026-10-10
• AI辅助完成11个正方形最优堆叠证明2026-10-07
• Bend：用证明阻断AI错误的编程语言2026-09-17