十月的第一个星期，数学界和 AI 圈同时看到了两份文件。一份是 OpenAI 的公告：把内部前沿模型产出的数学成果整理成仓库开源，GitHub 上的 openai/math 收录 722 份手稿、归并为 372 个结果家族，Hacker News 上一千二百多个赞。另一份来自剑桥的研究组，标题直白得像战书：Navier-Stokes lost in translation——为什么 Lean 验证过的 AI 自动形式化，并不能保证自然语言证明是对的。
这两份文件撞在同一周出现不是巧合。它们分别是 AI 数学这条流水线的「量产宣言」和「质检报告」。把它们放在一起读，才能看清这个行业正在发生什么。
一条数学成果的量产流水线
先看量产侧的数据，细节比标题更有信息量。
成本结构：绝大多数结果用同一套固定流程产出，使用一个未发布的内部前沿模型，平均每个结果约三小时 ChatGPT Pro 思考档算力。整个评估期间模型被提问约四千个问题，按显著性与聚合质量筛出 372 个家族。翻译一下这个经济学：单个结果的边际成本压到「几杯咖啡」量级，数学研究第一次具备了撒网式试错的条件——这正是前面 BOTTLED 基准在工程侧测的同一件事，只是对象从分类任务换成了定理。
内容光谱：公开的十份推理摘要横跨之广令人咋舌——圆周率的无理性指数、对称与一般 Mahler 猜想、特征 2 上的 Kaplansky 直有限性猜想、稀释自旋玻璃的 Mézard–Parisi 公式、量子海森堡铁磁体的自发磁化、自由群因子的同构问题、三维相对论性 Vlasov–Maxwell 方程。目录里还有两个特殊条目：黎曼 zeta 函数 Re(s) 大于 11/12 的零点自由区域（其写作经过了人工编辑润色），以及 CM 阿贝尔簇上的 Hodge 猜想。同一个模型在数论、代数、数学物理之间穿梭，这在人类数学家的分工体系里几乎是不可想象的配置。
同周的旁证：HN 上同日还热着两条相关线索——仓库里 9 月 23 日的预印本《低于 n log n 的整数乘法》，以及一个社区项目把「11 个正方形容器 packing 最优性」的 AI 辅助证明做了完整 Lean 形式化。前者改的是一个四十八年前被认为是下界的问题的常数项，后者展示了一个成型的工作流：模型提出构造，人类与证明助手共同压实。
验证层：Lean、协议与顾问组
量产必须有质检。OpenAI 的质检配置有三层。
第一层是 Lean 形式化：仓库附带形式化目录与验证配置，并承诺持续更新，「不是所有手稿都有形式化」这句免责声明被坦然写进了 README。第二层是发布协议：版本化保留全部历史、修订即新版本、附带引用与修订协议——这是把 arXiv 的预印本治理搬到了模型产出上。第三层是外部治理：与高等研究院旗下的数学与人工智能顾问组（AGM-AI）合作制定发布最佳实践，并探索社区托管的仓库方案。
值得注意的表述是 README 里那句「部分未形式化的结果可能有问题，我们会尽快修复」。这句平实的话背后是一个行业级共识的成形：模型产出数学成果的默认状态是「待验证」，而不是「已正确」。
反击：翻译鸿沟比停机问题更难
剑桥团队的论文（arXiv 2610.08144，2026 年 10 月 6 日提交）瞄准的正是这个「待验证」环节里最容易被高估的一环：自动形式化（autoformalisation）。
流程听起来很美：AI 把自然语言证明翻译成 Lean，Lean 是可以机械检验的，于是证明被「验证」了。Bastounis、Circelli 与 Hansen 的论证是，这个链条里藏着一步不可能完成的任务——消歧。自然语言数学充满省略与歧义，「显然」「类似地」「标准论证」背后是大量默认的语义约定；要把它们翻译成无歧义的形式语言，翻译系统必须正确解决所有歧义。而作者用可解性复杂度指数（SCI）层级证明：这个消歧问题在算术层级里的位置高到 SCI 等于无穷——形式上，语义保真的自动形式化比任何计算问题（包括停机问题，SCI 等于 1）都更难。
这不是纯粹的哲学抬杠。论文给出了实践中的 AI 翻译失配实例，矛头直指 OpenAI 公布的纳维-斯托克斯 blow-up 证明：形式化后的 Lean 证明与自然语言原证明并不对应——Lean 里验证通过的那个命题，不是原证明声称要证的那个命题。验证器说「对」的对象被悄悄换掉了。
把两份文件并排，争论的结构就清楚了：OpenAI 的立场是「多层验证加协议加透明度，逐步逼近可信」；剑桥的立场是「翻译这一步没有免费午餐，验证链的强度取决于最弱一环」。两者其实并不矛盾——但后者给前者画了一条清晰的线：Lean 勾是必要条件，远远不是充分条件。
给工程团队的四条启示
第一，验证链要分层设计。 形式化验证、专家审校、跨模型交叉检查、公开征求反驳，各自的成本与捕获的缺陷类型不同。OpenAI 把人工编辑过的写作单独标注、把有形式化和没形式化的结果分级呈现，这个「验证状态显式化」的做法值得所有 AI 产出管线照抄。
第二，「撒网-筛选」模式正在从代码走向科学。 四千个问题、三小时一个结果、372 个家族——这套流水线打法与去年以来智能体处理工程任务的演进同构。区别在于数学的筛选器（同行审议、形式化）比代码的筛选器（测试通过）弱，所以治理配套更重要。
第三，对「已验证」三个字保持职业怀疑。 任何「机器验证通过」的结论，都要追问验证的对象与原意之间隔了几层翻译。这条纪律适用于 Lean 证明，同样适用于 eval 分数、基准报告和自动化审计。
第四，发布即工程。 版本化、修订协议、引用规范、社区托管，OpenAI 这次示范的是「如何体面地公开一份不完美但可审计的成果集」。反过来说，剑桥一方的快速响应也说明，公开本身会召唤出高质量的对抗性审查——这恰恰是信任形成的机制。
结语
七百二十二份手稿是一面镜子，照出 AI 数学从「新闻」变成「产能」的速度；那一纸反驳也是一面镜子，照出产能背后验证体系的真实厚度。量产与质检的军备竞赛才刚刚开始，而胜负手不在谁的说法更响，在于验证链哪一环先被工程化地补齐。对旁观者来说，最实用的姿态或许是：为前者兴奋，为后者较真。