不跟 AI 比写证明，它改当验卷老师！AI 写的证明全是垃圾？这家初创用智能体给数学界最大资料库做了全量验证

大白话现在 AI 写数学证明又快又多，但很多看着像模像样、其实根本站不住脚，圈里管这叫「AI 垃圾」。Axiom Math 这家初创的思路是：不跟 AI 比谁写得快，而是让它当「验卷老师」，用机器能严格检查的形式化方式，把证明一步步核对到底。TechCrunch 报道说，他们的 AI 智能体刚把 Stacks Project 验证完了——这是代数几何领域体量最大的公开资料库之一。

对你意味着对搞数学、写论文的人来说，这关系到以后能不能信任 AI 给出的推导；对普通人，它决定了 AI 在科研里是帮手还是噪音制造机。