AI初创公司Axiom Math近日宣布，其AI智能体已完成对Stacks Project的形式化验证。Stacks Project是代数几何领域规模最大的公开文献库之一，汇集了大量定义、引理与定理及其证明，长期被研究者作为参考资源使用。此次验证意味着该文献库中的数学内容已通过机器可检验的逻辑校验流程。
这一进展的背景是，大模型正被越来越广泛地用于生成数学证明与推导内容，但生成结果缺乏可靠校验机制，未经证实的证明和似是而非的推理随之增多。Axiom Math将自身定位为这一问题的解决方案提供方，核心思路是用AI智能体承担形式化验证工作，将自然语言写成的数学论证转换为可被证明助手逐行检查的形式化代码，从而判断证明是否成立。
形式化验证并非新概念，Lean、Coq等证明助手已在学术圈使用多年，但人工形式化的成本极高，一个中等规模的定理往往需要研究者投入数天甚至数周。Axiom Math的做法是将这一过程交由AI智能体执行，以降低形式化的边际成本，使大规模文献库的整体验证成为可能。Stacks Project的验证规模在同类实践中较为少见，也构成对该方法可扩展性的一次实际检验。
从行业角度看，AI生成数学内容的可信度问题正在受到更多关注。此前已出现AI生成的证明在同行评议中被发现存在错误、或引用不存在文献的案例。若形式化验证工具能够以较低成本规模化运行，其应用场景可延伸至学术出版前的证明审查、教材与文献库的质量核验，以及AI数学推理模型的训练数据筛选等环节。
Axiom Math尚未披露此次验证的具体耗时、智能体调用规模及技术细节。形式化验证能否覆盖当前数学研究的主要产出，仍取决于自然语言证明到形式化代码的转换准确率，以及智能体在复杂推理链条上的稳定性。该案例为AI在数学质量控制环节的角色提供了一个可观察的样本。
该文观点仅代表作者本人，企服科学平台仅提供信息存储空间服务。
