一个开发布会，一个推代码

2026-10-29 · 人工智能

北京时间 10 月 27 日凌晨 4 点 52 分，OpenAI 的 GitHub 仓库多了一批文件。11 点 07 分，Anthropic 的仓库多了几个。

两次提交说的是同一件事：指数时间假设错了。

中间隔六小时。

一份配了五种仪式，一份只有一行免责声明

ETH，指数时间假设。1999 年由 Impagliazzo 和 Paturi 提出，大意是 3-SAT 这类问题没法在次指数时间内解决。过去二十多年，几百篇论文把它当前提，用它划定「这个问题不可能更快」的边界。

两家都说自家的模型推翻了它，而且都说是 10 月 16 日找到的。Anthropic 的论文里写了一句：OpenAI 的工作「独立且同时」。

然后就是两种交法。

OpenAI 那边：一篇公告，三条发布策略，四条原则，三位学者牵头，五百万美元捐给 Simons Foundation。Anthropic 那边：一个 commit，一篇论文，一份 Lean 形式化证明，Apache 2.0。没有博客，没有推文。

我不是说哪种更高尚。我是说，同一件事在同一天被做完，一家把它办成了一场学术外交，另一家把它当成了一次仓库更新。这个差别比证明本身更值得看。

那份不说话的 README

Anthropic 的论文叫《A 2^o(n) Time Algorithm for 3-SAT》，作者署名是「Claude (Anthropic)」。README 里有一句来源说明：核心算法是 10 月 16 日由内部的 Claude 研究模型找到的，1400 万输出 token，全程没有人工输入。

它比 OpenAI 那份还多做了一步。3-SAT 问的是「有没有解」，它顺手把更难的那题也做了——数出有多少组解，时间 2^O(n log log n / √log n)。会数，自然就会判有没有。

但真正让我停下来的是 README 里的另一句，原文是：Lean checks the proofs, but no machine checks that this file says what the paper says.

Lean 验的是证明，没有机器验这个文件说的就是论文说的。

所以那个 MainResults.lean 被故意写得很短，短到一个人可以肉眼跟论文对一遍。CI 里还跑了第二个独立写的核，叫 nanoda，把证明再重验一次。

这句话是这次两场发布里，唯一一句承认自己还没验完的话。

而且它写在没开发布会的那份里。

顺便说清它有多没用：这个界只在变量数超过 10 的 108 次方时才开始赢过暴力枚举。现实里的 SAT 求解器，一行代码都不用改。论文自己写得很清楚——纯渐近，不谈实践。

一个没有实用价值的结论，被作者用最朴素的方式交出来：能验的给你，验不了的我自己说。

出题的人来收卷

再看 OpenAI 那份。

10 月 26 日的公告里，三个结果配了三种交法：数学的直接放出来，让学界自己组织解读；计算机科学的组一个外部小组来解释，材料同时公开；物理的听小组的——小组说先别发，那就不发。

物理那份的时间线是这样的：9 月 9 日模型给出杨-米尔斯存在性的自然语言证明，9 月 18 日给出 QCD 的，10 月 16 日才完成 Lean 形式化。领衔的是 David Gross，1973 年那套渐近自由的工作给他挣了 2004 年的诺贝尔奖。组里还有 Arthur Jaffe——和 Witten 一起把「杨-米尔斯存在性与质量隙」写进克雷千禧年清单的人。

出题的人来收卷了。

而且这份卷子还少答了一问。千禧年那道题要两样东西：存在性，和正的质量隙。OpenAI 只交了存在性。公告里没提质量隙，别处也没提。

有人不高兴。《The Verge》采访了得州大学奥斯汀分校的 Andreas Karch，原话是：他们手挑这个组，是一场灾难。

这话不算刻薄。10 月 25 日，也就是 OpenAI 发公告前一天，Timothy Gowers、Martin Hairer 这些人组成的数学与 AI 咨询小组发了一篇文章，标题就叫《指定数学家参与 AI 成果发布的弊端》。理由很实在：让少数人先看到成果，会造成信息不平等；而科学家的名声，很容易在不知情的情况下变成对未审结论的背书。

OpenAI 自己也承认这一点。公告原文写：选定最初的「牧羊人」，必然决定了谁先参与，并造成信息不对称。欢迎就如何扩大参与提供反馈。

一个公司把自己的软肋写进公告，这件事本身就少见。

再看那三位牵头核查 ETH 的学者。Impagliazzo、Paturi、Ryan Williams，公开信里第一句就是：我们的参与不应被视为对该主张的认证。

Williams 在社交平台上补了两条：没签保密协议，不拿报酬。他们还要求 OpenAI 公开全部原始材料、出资办一场讨论会——都答应了。那五百万美元是给 Simons Foundation 一个新倡议的，那个倡议总共一千五百万，用来办工作坊和会议，让人有时间去读懂这些东西。

公开信的资源清单里，Anthropic 那份证明和 OpenAI 那份并排列着。

前科这件事，绕不过去

要理解为什么这次这么小心，得翻一下这个月的账。

10 月 6 日，OpenAI 一次性放出 721 篇手稿，归成 373 个族。仓库 README 自己写的数字，还说平均每个结果用了 3 小时 ChatGPT Pro 的思考算力，前后喂了大约 4000 道题。第二天就撤了三篇——一个符号错误，废掉一个论证和两篇依赖它的。

再往前，还有一次说 GPT-5 解决了 10 个 Erdős 未解问题。维护那个问题库的 Thomas Bloom 出来解释：模型只是翻出了他自己没读过的旧论文。

还有一次是 Navier-Stokes。数学家 Tristan Buckmaster 说，OpenAI 用的方法他和同事早就在做。

最要命的是第四件。剑桥的 Anders Hansen 和合作者写过一篇论文，论证 Lean 形式化可以编译通过、却跟它本该对应的自然语言证明不是一回事。他们举的案例，就是 OpenAI 的 Navier-Stokes 工作。

这条正好戳在今天的软肋上。两份 ETH 证明都过了 Lean，可 Lean 只保证「从这个陈述能推出那个结论」，不保证「这个陈述就是论文里那句话」。

Anthropic 在 README 里把这一层挑明了，OpenAI 没提。而 OpenAI 的仓库里，721 篇手稿只有大约 42% 的顶层结果做了形式化——剩下那一半，连机器都没碰过。

谁签字

两份证明现在还躺在两个仓库里，谁都能下载。

一份旁边站着三位学者、四条原则、五百万美元、一场还没开的会，还有一篇写了「我们不为发现索取学术荣誉」的公告。另一份旁边只有一行字：没有机器验过这个文件说的是不是论文。

我盯着这个对比看了很久。

前一份把学术界的仪式做全了，从透明到独立到不抢功，每一条都写得很体面。后一份什么都没做，只是把能验的东西摆出来，然后老实说哪一块还没验。

这两件事不冲突。可我总觉得，如果有一天这些证明里有一份是错的，我们会更快知道是哪一份。

因为错的会被 build 失败抓住。

而另一份，得等五个很忙的人抽出时间，先把论文写出来。