AI 生成数学证明没人核，Axiom Math 想把 7,654 页文献变成机器可查的代码
作者：周砚
Axiom Math 宣布其 AI 智能体把 Stacks Project 约 7,654 页文献翻译成约 1,600 万行 Lean 代码，交由证明助手逐行检查。公司称这为代数几何补上了形式化基础，但验证范围、独立复核、收费模式均未披露。
11 月 4 日（周三），Axiom Math 宣布其 AI 智能体完成了 Stacks Project 的形式化验证：这套约 7,654 页、由数学家志愿维护二十余年的开放文献，被翻译成约 1,600 万行 Lean 代码，再由证明助手逐行检查 。变化在于：AI 生成的数学证明越来越多，且真假难辨，而这批文献第一次以这个体量变成机器能核验的对象 。TechCrunch 称，这家公司估值 16 亿美元 。
给证明上质检锁
形式化验证的做法，是把证明里的每一步推理写成 Lean 代码，交给证明助手逐行查。人审稿像抽检成品，难免漏检；机器检查则要求每个环节都有出处，某一步用了没写明的假设，或者两个定义互相打架，代码就过不去 。芯片设计早就是这么验的，法国研究者也用它找出过家庭补助计算软件里的 bug 。
Stacks 的难点在于依赖关系，而不在单条定理。定理和定义层层相扣，就像一棵家谱树，1,600 万行代码里断掉一处，下游就全部作废 。CEO Carina Hong 说，团队起初并没有把握。办法是给智能体一个“松散的层级”和并行目标，让它们自己找活干，同时用自研模型补数学能力，早期由内部 Lean 专家教它们“品味” 。技术团队成员 Ashvin Swaminathan 说，代数几何此前几乎是形式化数学里的一块空白 。
公司 2025 年 3 月成立，Hong 25 岁，从斯坦福数学博士项目退学；今年 3 月完成 Menlo Ventures 领投的 2 亿美元 A 轮 。
谁买单
受众分两层。近处是数学家：想用 Lean 检查代数几何新工作的人，过去缺少可依赖的基础库 。远处是写代码的人：AI 智能体写下的代码越多，“保证没有漏洞”越难，Axiom 的说法是让未来的软件也站在可验证的地基上 。这条路径和芯片业的验证工具生意类似：先有可复用的检查层，再谈规模化 。
收费方式还不清楚。报道没有披露它按项目收费、订阅收费，还是以开源换生态，也没有提到任何已签约客户 。2 亿美元 A 轮说明它有做长周期研发的余地，16 亿美元估值则说明投资人相信这个市场会长出来 。前者是耐心，后者是预期；两者能不能对上，要看它把“能验证”变成“有人愿意付钱验证”有多快。
几处需要留个心眼
验证结果是公司自己宣布的，报道中没有独立第三方复核 。“verified”的具体范围也没讲清：是全库定理编译通过，还是连定义与依赖链一起完整重建；Lean 版本、人工介入比例、耗时，报道均未提及 。代码是否公开、别人能否复现，同样没说 。
数字上有一条能对上：Stacks 官网标注 7,654 页，与公司口径一致；但官网的 76.7 万“行代码”指原文献的 LaTeX 源码，和 1,600 万行 Lean 不是一回事 。官网还显示，项目仍由人工维护，最近一次提交在 7 月 28 日，10 月 21 日发过一篇题为《No AI for now》的博客——这篇文章写了什么，公开页面上看不到，也不宜直接读成对 Axiom 的回应 。
菲尔兹奖得主 Terence Tao 的说法可以当作这门生意的底层假设：“形式化证明越多，能做出的形式化证明就越多。” 假设成立，先做好基础库的人拿的是复利；不成立，这就是一笔很贵的公共品投入。
转载说明
本文根据以下公开资料整理，原文及配图出处见下方。
评论 0
还没有评论，来抢沙发。