Axiom Math用AI形式化验证Stacks Project，阻击数学「AI垃圾」

AI生成内容正在涌入数学领域，大量未经严格审查的证明随之而来。面对这一趋势，初创公司Axiom Math选择了一条不同的路：用AI智能体为数学证明做形式化验证。据其披露，该公司的AI智能体已完成对Stacks Project的形式化验证——这是数学领域规模最大的文献库之一。

Axiom Math相关报道截图

数学领域正在面临「AI垃圾」问题

大语言模型写证明的速度远超人类审阅的速度。一篇结构看似合理、符号使用规范的证明，可能在关键推理步骤上存在隐蔽漏洞，而这类漏洞未必能被快速阅读发现。当AI生成的证明大量涌入预印本平台和学术交流渠道，数学界面临的不是「没有内容」，而是「内容太多且真假难辨」。

Axiom Math将这一现象称为数学领域的「AI垃圾」（AI slop），并认为仅靠同行评审的人工流程已经难以应对。验证，而非生成，成为更紧迫的环节。

形式化验证的核心思路，是把数学证明翻译成机器可以逐步检查的形式语言，再由验证器逐条确认每一步推理是否合法。与自然语言证明依赖读者理解不同，形式化验证给出的是可机械复核的结论：证明成立，或者在某一步不成立。

这条路线并非新事物，但长期受限于人力成本——把已有数学文献形式化是极其繁重的工作。Axiom Math的切入点是用AI智能体承担这一翻译与验证过程，从而把形式化验证从「少数项目可做」推向「大规模文献可做」。

形式化验证依赖的核心工具是证明助手（proof assistant），也称交互式定理证明器，代表性系统包括Lean、Coq和Isabelle。这类系统内置一套基于类型论或集合论的形式逻辑内核，用户用其专用语言书写定义、引理与证明，内核逐条检查每步推理是否由前序步骤和公理合法推出。

与自动定理证明（如SAT/SMT求解器）不同，证明助手不负责"想出"证明，只负责"把关"证明；证明的构造仍由人或AI完成。Lean的数学库mathlib是目前规模最大的社区共建形式化数学库，已积累数十万条定理，可作为理解"形式化验证已能做到多大体量"的现实参照。

Stacks Project是代数几何领域的重要文献库，体量大、结构复杂，长期被视作形式化验证的硬骨头。Axiom Math的AI智能体完成对其的形式化验证，说明智能体在长程、多层依赖的数学文本上具备可用的处理能力，而不仅仅是做短小的习题级验证。

这一结果的实际价值在于建立可信基线：当相当规模的既有数学内容已被形式化，新出现的AI生成证明就有了可对照的验证环境，而不必每次从零构建检查体系。

Axiom Math验证工作示意

Stacks Project由哥伦比亚大学的Johan de Jong发起并持续维护，是一部以代数几何与代数栈理论为主题的开放式在线文献，包含数千个标签化定义、引理与定理，章节之间存在大量跨节引用，依赖关系呈深度嵌套的图结构。

这种"长程依赖"正是形式化验证最棘手的地方：验证一条后期定理，往往需要先形式化它依赖的全部前置结果，任何一环缺失都会使检查中断。因此，完成对Stacks Project的形式化，不只是处理体量问题，更是处理依赖闭包问题，这也是该结果被视为难度标志的原因。

Axiom Math的定位并不是与生成式模型竞争写证明，而是把验证做成基础设施。这一分工有其现实逻辑：生成的门槛在降低，验证的稀缺性在上升。谁能提供低成本、可扩展的验证能力，谁就掌握了AI数学内容质量的关键环节。

当然，形式化验证也有边界。它验证的是「证明在其形式化表述下成立」，而形式化翻译本身是否忠实于原始数学意图，仍是需要人工把关的环节。Axiom Math的方案能否在更大范围文献上稳定复现，也需要更多公开结果来检验。

对于关注AI在科学研究中落地的读者，这一方向提供了一个值得跟踪的样本：AI不只是产出内容，也可以成为内容的把关者。