ARTICLE · 1139705
OpenAI甩出722份手稿,数学界:Lean通过≠证明对
OpenAI甩出722份手稿,数学界:Lean通过≠证明对10月6号半夜，OpenAI往GitHub上扔了个仓库，名字简单粗暴，叫openai/math。里面躺着722份数学手稿。 我第一反应不是去数有几份，是赶紧翻数学圈的反应。 结果翻到一条声明，看完第一段我就愣住了。这声明不是别人发的，是AGMAI，一个OpenAI自己花钱请来、专门给自己数学成果把关的顾问团。 它上来第一句话就是：别把我们当背书。 先把这个数字摊开说清楚。 OpenAI这次发布的，是722份手稿（他们自己用的词是manuscript，手稿），归成372个结果族，来自大约4000个待解问题的评测，平均每个结果花掉约3小时ChatGPT Pro级别的思考算力。 产出的模型是谁？一款还没发布的内部模型。模型本身不给，只给结果和部分Lean形式化证明。整个仓库用了Apache-2.0协议开源，谁都能下载。 覆盖的方向确实唬人：米尔恩理性猜想、准黎曼假设、希尔伯特第十问题，还有那篇被单独点名的Navier-Stokes方程爆破证明。 这堆名字，圈外人可能没感觉，我说人话解释两个。 准黎曼假设，是黎曼假设的一个亲戚。黎曼假设是数学界公认的头号悬案，一百多年没人攻下来，谁要真证了，菲尔兹奖和一百万美元的千禧奖金直接到账。准黎曼这个"亲戚版本"要是被AI"解决"了，意味着什么，你感受一下。 希尔伯特第十问题，问的是有没有一个通用算法，能判断任意一个丢番图方程有没有整数解。1970年已经被证否了：不存在这样的算法。OpenAI这次碰的是它衍生出来的一批子问题。 听懂这一层，你才知道OpenAI这次选题有多精。它挑的全是"够分量、够难、但又不是完全无解"的靶子，每一个都自带流量。 注意一个词：手稿。 手稿不等于论文，论文不等于被验证的定理，被验证的定理也不等于被数学界认可、进了教科书。这中间每一环都是一道门槛，OpenAI这次是想一次性把门槛全跨过去。 那数学界的反应呢？ 数学界第一反应，是官方级别的撇清 AGMAI是谁，得先交代清楚。 9月21号，OpenAI官宣成立这个"数学与AI顾问组"，说它会"有自由提出我们没要求的建议，评论OpenAI对数学的影响，并把建议公开"。 9月29号，AGMAI发了一份"负责任发布"指南，三条：别再用闭源模型去测前沿难题；实验室得掏钱资助人类去理解那些看不懂的AI证明；还警告了一句，如果模型访问一直封闭，数学界会裂成两套体系，一套玩得起算力的，一套玩不起的。 然后10月6号，OpenAI发布了。当天，AGMAI发声明。 声明第一段，我逐句给你拆： "AGMAI的咨询角色不应被解读为对这些结果影响的评判，也不应被解读为对OpenAI获取这些结果过程的认可。" 翻译成人话：我们只是被请来当顾问的，别以为我们给这批成果盖过章。 更狠的是下一句："我们不代表整个数学界，只有数学界才能做所需的评估。" 再往下还有一段，我读完直接笑出来了： "把这项工作公开只是第一步。这次发布是开始，不是结束。数学的未来不能只靠理解AI实验室产出的结果。数学家必须能自己提出问题、自己找方法、自己去探索那些没有被AI当作能力展示例子选出来的方向。公平获取强大研究工具和足够算力，对这份自由至关重要。" 你品品这个味道。OpenAI花大价钱请来的顾问团，在OpenAI发布成果当天，公开说"你们自己玩，别绑架整个数学界"。 更黑色幽默的是，AGMAI这个顾问团，本身就是OpenAI官宣成立的。换句话说，OpenAI花资源养了一个班子，这个班子上任第一件大事，就是公开跟它划清界限。这在科技圈的历史上，几乎是独一份的待遇。 我翻了几十篇报道，中文英文都看了，没人把这件事的本质讲清楚。 大家都在吵"AI到底有没有攻克这些难题"，吵"722份里有多少是真货"。这个角度已经被写烂了。 我看真正的戏，在发布权。 OpenAI为什么要主动把流程送交AGMAI？它完全可以像之前甩模型评测一样，直接发个博客就完事。它偏要绕一圈，先成立顾问团，再让顾问团出指南，再带着722份手稿去交作业。 因为它缺一样东西：一个合法的发布通道。 数学和别的领域不一样。一篇数学结果要"算数"，得经过一套几百年打磨出来的机制。先上arXiv让大家挑错，再投期刊，再等同行逐行读你的证明。这套机制的权威，是建立在"证明被人类读懂"这个地基上的。 OpenAI这次直接绕过这套机制，把4000个问题的结果一次性倒出来，本质是在问数学界一个很尖锐的问题：能不能给我开个新的、更快的通道？ 它的潜台词是：我连数学这个最硬的领域都能量产结果了，你要不要跟我坐下来，重新谈一套"怎么判定AI结果算不算数"的规则？ 所以722这个数字，真正的功能不是炫耀能力，是谈判桌上的筹码。 这事有前车之鉴，就是四色定理。1976年Appel和Haken用计算机跑了一千多个小时，把四色问题给"证"了。结果接下来十几年，数学界一直不认账。不是结果错了，是没人能从头到尾把那份计算机证明读一遍。直到后来有了独立的形式化验证，大家才勉强接受。四色定理从"证出来"到"被承认"，中间隔了几十年。 OpenAI现在想用722份手稿，把这几十年压缩成几天。数学界不干，再正常不过。 AGMAI的撇清，就是看穿了这一手。它一边拿着OpenAI的名分和资源，一边死守一句话：谁说了算，不是你能定的。 如果只有OpenAI的发布和AGMAI的声明，这事还停留在权力斗争的层面。真正把它锤死的，是当天arXiv上同批出现的一篇论文。 这里得先补一课，不然后面看不懂。 Lean是个什么东西？它是个证明助手，说白了是数学界的一门编程语言。数学家用它把一条定理和它的证明，像写代码一样逐行敲进去，每一行都得符合严格的逻辑规则。敲完了，电脑会一行一行检查：这一步到下一步，逻辑上是不是真的推得过去。 这套东西的价值在于，电脑不会打盹，不会跳过细节，不会因为"看起来对"就放你一马。所以一旦Lean说"通过了"，你就知道：这份形式化的证明，内部是没有逻辑漏洞的。 那问题出在哪？出在"翻译"这一步。 回到那篇论文。编号2610.08144，标题我照原文翻：Navier-Stokes lost in translation，翻译成中文是"Navier-Stokes在翻译中丢了"。副标题更直接：为什么Lean验证了AI的形式化证明，却不保证自然语言证明是对的。 作者Bastounis等三个人，25页，4张图。 他们证明了一件听起来很绕、但结论很硬的事： 把自然语言数学"忠实翻译"成Lean，这个过程里最难的一步，消歧义，处在SCI=∞的位置。SCI是"可解性复杂度指数"，用来给计算问题分难度档。停机问题已经算难的了，它的SCI是1。而"把数学文本翻译得语义忠实"这件事，难度是∞，比停机问题还高。 用大白话说：让机器"证明"一个结论，和让机器"确认它证明的还是不是原来那个定理"，是两件难度天差地别的事。 停机问题已经够难了吧？图灵1936年就证明，不存在一个程序能判断任意程序会不会死循环，这是计算机科学的基石结论。而这批数学家说的是：忠实翻译数学这件事，比判断死循环还难，难到没法用任何有限的算法步骤去逼近。 换句话说，OpenAI号称"我们让AI把证明都形式化验证了"，背后默认了一件事：翻译是可靠的。这篇论文直接把这个默认拆了。 Lean能保证的只有一件事：被形式化的那一份证明，逻辑自洽。它保证不了另一件事：这份形式化的东西，跟你原来用自然语言写的那个定理，是不是同一个意思。 论文直接点名OpenAI那份Navier-Stokes爆破证明，说他们检查了，形式化版本和自然语言里的爆破证明，根本对不上。 这就是我开头说的那句话：验证机器过了，不等于定理对了。 论文是理论层面的冷水，社区里还有一个实测层面的。 有开发者把OpenAI那个"准黎曼假设"的结果拿去重跑，用的是双内核验证，跑完2924个模块，零报错。 听起来很硬。结果他补了一句，这句话是整件事里最锋利的一句注脚： "this checks the Lean proof, not the paper。" 翻译：这检查的是Lean证明，不是论文。 这里解释一下那个"双内核"和"比较器配置"是什么意思，不然容易看走眼。 形式化验证里，内核是负责做最终判定的一道独立程序。设计它的初衷是：既然AI可能出错，那就用两套不同的内核分别去验一遍，两个都说"对"，才算对。这就叫双内核，用冗余换可信。 比较器配置呢，是控制内核怎么判"通过"的一组开关。405个比较器里，404个默认把第二内核关掉了。翻译过来就是：这套"双保险"，绝大多数时候其实只有一重保险在转。 所以那个"零报错"的漂亮结果，建立在一个打了折的验证标准上。开发者那句"checks the Lean proof, not the paper"，说的正是这个：即便这一重保险是真实的，它也只在"形式化那一份内部自洽"这件事上负责，出了这个圈，它一个字都不认。 说完海外的冷水，说说这事对国内意味着什么。我不觉得是坏事，反而有个很实际的机会。 普林斯顿一个叫Goedel-Architect的团队，拿DeepSeek-V4-Flash去跑PutnamBench，672道题全跑完，API账单是294美元，通过率75.6%。对照谷歌的Hilbert系统，跑同样的东西花了约17万美元，通过率70.0%。 花别人零头的零头，通过率还反超。这一条信息，比OpenAI那722份手稿值钱多了。 它说明一件事：数学AI这个战场，真正在变的不是"谁证明得多"，是"验证这件事突然变便宜了"。 为什么说这对国内尤其是个机会？拆开看。 验证的成本分两块。一块是算力，跑Lean、跑形式化检查，一分钱一分货，这块我们熟，价格战打法直接套用，Goedel-Architect的294美元就是现成的例子。另一块是人力，一个顶尖数学家读懂一份几百页的AI证明，这成本不可压缩，也是最贵的。 过去这块人力成本堵住了整个行业的脖子：AI产出的证明越多，人类越读不完，瓶颈越紧。DeepSeek这条线证明的是第一块能被打穿。第二块，正是国内这几年在攒的东西：大量接受过严格数学训练的毕业生、越来越成熟的国产形式化工具链。 这条线的价值，不在于追上OpenAI的证明产量，而在于卡住"验收"这个咽喉。产量可以拼算力，验收拼的是人力和信任。信任这东西一旦建立，迁移成本极高，后来者想撬都撬不动。到那时候，一份"经过XX验证"的证明，会像今天的审计报告一样，变成一种可以反复收费的凭证。 陶哲轩最近反复说一个判断：数学已经从证明稀缺进入证明过剩，瓶颈从"做出来"转到了"验明白"。谁先把"Lean工件和人类证明之间对应关系"的检查自动化，谁就能把第二块成本也打下来。到那天，验证就不再是数学界的贵族特权，而是一门可以规模化交付的服务。 这件事不需要什么惊天动地的技术突破。它需要的是一套把"形式化证明"和"人类论文"逐段对齐的工具，一份能自动标出"这一段Lean对应论文哪一节"的报告。谁做出来，谁就是数学AI时代的质检员。质检员这个位置，在任何行业里都是躺赚的。 "让验证变便宜"，这是一门生意，而且已经有人开始赚钱了。 再落到具体的人身上，给正在做、或者打算做AI for Science的人。 以后你们团队要是采信一份"AI证明"，交付件必须凑齐三样东西： 第一，Lean工件，就是机器能跑、能复现的那份形式化证明。第二，人类可读的证明，让一个合格的数学家能从头读懂的那份。第三，也是最重要、最容易被省掉的，一份声明，写清楚前两样东西之间的对应关系：这份Lean，到底形式化的是不是这份人类证明里的这个定理。 举个具体例子。你们团队用AI证了一个定理，拿到一份Lean文件，机器跑过了。这时候交付单上写"证明完成"，错。正确写法是三行。一行写Lean工件：某文件，可通过。一行写人类证明：下面这段。第三行写对应声明：这份Lean形式化的对象，是上述人类证明里的定理X，不是定理Y。 第三行看着像废话，恰恰是整个链条上最难、也最容易糊弄的地方。因为翻译这一步，本身就是最难的那一步。 缺第三项，按未验证处理。不是打折扣，是直接当没验证。 为什么非要第三项？因为Bastounis那篇论文已经用数学证明了：翻译这一步是整个链条上最难的环节，比停机问题还难。你把最难的一步当成"理所当然成立"跳过去，后面验证得再漂亮，都是在给一个可能对不上的东西盖章。 还有一句要补的：形式化验证工具链，现在就是明码标价的付费需求。谁先把这个"对应关系"的检查做成工具、做成产品，谁吃的是真金白银，不是概念。 回到开头那722份手稿。 OpenAI想买的，是一个"我说结果算数"的快速通道。AGMAI想守的，是"只有数学界说了算"的定义权。两边都聪明，都清楚真正的战场不在那几个定理对不对，在于将来谁的"证明"能直接进教科书。 722不是能力证明，是谈判筹码。筹码越大，谈通道的时候嗓门就越大。 而数学界回的那句"这检查的是Lean证明，不是论文"，我建议每个关注AI的人记下来。它可能是接下来十年，所有"AI又搞定了X"新闻的万能解毒剂。