AI写出一篇像模像样的数学证明，不等于它真的算对了，就像学生交来一整页推导，老师仍要逐行验算。随着机器批量生成证明，数学界面对的麻烦也从“AI会不会做题”，变成“结果能不能可靠检查”。据 TechCrunch 报道，Axiom Math 宣称已完成 Stacks Project 的形式化验证：这部持续更新的代数几何参考资料约有7654页，被转换成约1600万行可由计算机检查的代码。
Axiom使用 Lean——一种编写形式化证明的语言——重写其中的定义、引理和证明，再交给证明助手逐步核对逻辑。难点不只在验证单个定理，还要保住它们之间层层引用的关系。公司让一批AI Agent在一个较宽松的层级结构下并行寻找任务、协同推进。
这件事值得关注，不是因为AI又“解出一道难题”，而是它试图搭建一套可验收的数学底座，让后续Agent交出的证明不只看起来专业，还必须过机器审查。不过，目前完成规模与效果主要来自Axiom及TechCrunch报道，材料未披露独立复核结果。