Axiom Math：给AI数学证明当"验货员"

编者按：当AI开始以惊人速度"生产"数学证明，一个尖锐的问题摆在数学界面前：这些证明，哪些是真的？创业公司Axiom Math给出的答案是——用机器验证机器。

一、AI涌入数学，带来"证明洪水"

过去两年，大语言模型在数学领域突飞猛进。从解答奥数题到辅助证明猜想，AI展现出的能力令数学家既兴奋又不安。兴奋的是，AI可能成为强大的研究助手；不安的是，AI生成的证明往往"看起来很美"，却可能在某个不起眼的步骤藏着致命错误。

数学是一门要求绝对严谨的学科。一个证明要么完全正确，要么一文不值，没有中间地带。传统的同行评审体系依赖人类专家逐行审读，但面对AI以分钟为单位产出的海量证明，这套体系已经不堪重负。有人将这种现象称为数学界的"AI slop"——大量低质量、未经核验的内容涌入，稀释了学术共同体的信任基础。

二、形式化验证：让机器检查机器

Axiom Math选择了一条技术门槛极高的路径：形式化验证（formal verification）。所谓形式化，就是把数学证明翻译成计算机可以逐步检查的代码，借助Lean、Coq、Isabelle等证明助手，确保每一步推导都严格符合逻辑规则。任何细微的漏洞都会被机器毫不留情地揪出来。

这与传统的"读证明"有本质区别。人类审稿人会疲劳、会遗漏，也可能被华丽的论证结构说服；而形式化验证器只认逻辑。它不在乎证明写得多漂亮，只在乎每一步是否成立。

"数学的本质是可验证性。如果一个证明无法被机器检验，那它在AI时代就很难被信任。"——这是形式化数学社区长期秉持的信条。

Axiom Math的核心创新在于用AI代理自动化这一过程。传统上，形式化一个复杂证明需要专家投入数月甚至数年时间，成本高得令人望而却步。Axiom Math希望让AI承担繁重的翻译和验证工作，把人类数学家解放出来，专注于真正需要创造力的部分。

三、Stacks Project：一块硬骨头

此次完成的Stacks Project，是代数几何领域最庞大的开源文献工程之一。该项目由哥伦比亚大学数学家Johan de Jong发起，旨在系统整理代数叠（algebraic stacks）及相关理论，内容横跨数千页，涉及大量高度抽象的概念和定理。

选择Stacks Project作为验证对象，颇具象征意义。它既是现代代数几何的基础设施，也是检验形式化技术能力的"试金石"。如果AI能够处理这样规模庞大、结构复杂的数学文献，那么形式化验证从象牙塔走向规模化应用就有了现实可能。

当然，完成验证不等于一劳永逸。数学知识在增长，文献在更新，验证系统需要持续维护。但至少，Axiom Math证明了这条路走得通。

四、赛道渐热：形式化数学的"军备竞赛"

Axiom Math并非孤军奋战。近年来，形式化数学正在成为AI领域的新战场。Lean社区的mathlib库不断扩充，菲尔兹奖得主陶哲轩（Terence Tao）等人积极推动数学形式化；DeepMind、OpenAI等巨头也在探索用AI辅助定理证明。

背后的逻辑不难理解：如果AI生成的数学证明能够被自动验证，那么AI辅助数学研究的可靠性将大幅提升。这不仅是学术问题，也关乎AI在科学发现中的可信度。谁能率先建立起高效、可靠的形式化验证流水线，谁就可能掌握"AI for Science"时代的关键基础设施。

五、挑战仍在：成本、规模与接受度

尽管前景诱人，形式化验证的普及仍面临多重障碍。首先是成本：即便有AI辅助，形式化一个复杂定理依然耗时耗力。其次是生态：并非所有数学分支都有成熟的形式化库，标准也不统一。第三是文化：许多数学家仍习惯纸笔证明，对机器验证持观望态度。

此外，"验证什么"本身也是个问题。AI可以生成无穷无尽的证明，如果全部都去形式化，算力成本将难以承受。Axiom Math需要建立一套筛选机制，判断哪些证明值得验证、哪些可以直接丢弃。这本身就是一个涉及数学品味和工程判断的难题。

结语

AI让数学证明的生产变得廉价，但信任从来不是廉价的。Axiom Math的尝试，本质上是在为AI时代的数学重建信任基础设施。Stacks Project的验证只是一个开始。当形式化验证变得足够便宜、足够快，数学研究的面貌或许会被彻底改写——到那时，数学家不必再担心被"AI垃圾"淹没，因为每一份证明都要先过机器这一关。

本文编译自TechCrunch