都说 AI 证了三大难题，有一项连论文都没有

Hello，我是飞飞。

三项里有一项，论文和 Lean 都没公开。转得最广的那句话没提这一句。

这三项差着三档。差别就在三样材料上：论文、Lean 证明、外部专家。传到你耳朵里的「AI 一口气解决了三个大难题」，把三件不同的事压成了一件。

三项成果不是一档

	数学	计算机科学	物理
论文	公开，59 页	公开，67 页	没公开
Lean 证明	公开	公开	没公开
外部专家	没组，只问了一位不具名的人	三人组	五人组，Gross 领衔
专家结论	没有	公开信说参与不等于认证	没有，自己写论文
同行评议	零	零	零

Lean 是专门写证明的语言。证明翻成它能读的代码，编译器一步一关地查，哪一步接不上就报错。

OpenAI 官方自己交代了三套发布办法。数学那套的原话是「release the AI output, leaving researchers free to organize their own efforts」。说白了就是，把输出放出去，研究者自己组织人去解释。The Decoder 把这句读得更直白：No dedicated shepherd group was formed，没有专门组建领读组。

所以「三项都请了专家核查」这个说法，在官方原文里找不到。官方请专家干的事，动词是 understand，理解。这跟核查不是一回事。

原文和转述差在哪

先看数学这项。

Kakeya 说人话：一根单位长的针在平面上转 180 度，每个方向都指过。它扫过的那块地方，能有多小？面积可以小到接近零，数学家就换个问法：维数能不能也塌下去。猜想说，不能。

还有一条限定不算放大，但引用时容易漏。论文证的是二维及以上的所有维度。一维是平凡情形，论文和 Lean 都排除了。

真正被放大的是 Stein 限制猜想。论文摘要的原话是 throughout the interior of the conjectured range，猜想的区间内部。官方博客把它简化成 resolve in all dimensions。区间内部不含端点。说它连端点一起解决，是错的。

另一处是那句「推翻了 ETH」。

ETH 本身是一条信念：3-SAT 这类逻辑题，最坏情况下一定得花指数时间。指数还不能太小，得跟 n 成正比。它不是定理，可过去二十多年，几百篇论文拿它当地基。论文给的是一个确定性算法。它能精确数出一类逻辑公式有多少组解，这类公式叫 k-CNF。能数清有几组解，就能判有没有解。一个数解的算法，等于一个判解的算法。它花的时间比 2 的 n 次方少一截，可 ETH 要的正是这条硬线。线被压下来，ETH 就假。要精度的话，那个「少一截」是 2 的 O(n loglog n 除以根号 log n) 次方。

这两件事得分开。推翻 ETH 推不出 P 等于 NP。论文自己写死了：our result does not imply that general NP problems admit subexponential time algorithms，我们的结果不蕴含一般 NP 问题有次指数时间算法。更细的一层是，Lean 里验的那条比论文主定理还弱一档，指数里多一个 log log n。两边的界都足以否定 ETH。可你要是只看 Lean 文档，会以为它验的是最锐的那句。

物理这项，官方只写了 part of。原文说纯杨–米尔斯的存在性，是千禧年难题的一部分。

杨–米尔斯这套理论，物理学家拿它算强相互作用，算得极准。可数学上没人证明它作为一个严格对象真的存在。也没人证明它有质量间隙。质量间隙是说，这套理论预言的最轻那颗粒子得有分量。不能一路轻到零。Clay 研究所悬赏的一百万美元要两样都有。官方公告全文没有出现 mass gap 这个词。存在性这一半，他们给了证明；质量间隙没碰，钱拿不到。

材料也不在。论文没公开，Lean 没公开，五人组自己写论文，不放出来。哥大数学系的 Peter Woit 在博客里问了一句：这个「存在」，会不会只是有限体积下的？这是博客里的质疑，不是学界定论。

剩下一项最朴素：三项都没有同行评议。官方全文找不到 peer review、preprint、not yet peer-reviewed 这些词，用的是 raw research data，原样研究数据。两篇公开的论文里没有致谢，署名只有 OpenAI。其中一篇连 AI 生成声明都没有。

三项背后是七百篇

发布单位根本不是三篇论文。

仓库里躺着 721 篇手稿，373 个结果族。这次的三项，是从里面拎出来的三个条目。约 42% 的主要结果有 Lean 形式化，反过来读，六成没有机器验证。官方自己写：Some of the unformalized results could have issues，没形式化的结果可能有问题。

这批东西怎么来的？平均每个结果烧 3 小时 ChatGPT Pro 的思考算力，前后喂了大约 4000 道题。10 月 7 日，因为一个符号错误，连带撤了 3 篇。

所以「Lean 验过了」这句话，在数学和计算机科学这两项上，能成立的范围只有一句。证明和论文写的那条陈述对得上。对那个库，连这一句都还不成立。库的状态是开始验了，验了四成出头。

同一天还有另一家

10 月 26 日不止一家在动。Anthropic 放出一篇论文，同样宣称推翻了 ETH，署名是 Claude (Anthropic)。

核心算法 10 月 16 日找到，和 OpenAI 撞在同一天。1400 万个输出 token，官方说发现过程没有人类输入。同样给了 Lean 4 形式化。README 里逐条标了论文陈述对应哪段 Lean、哪里不一样，跑了 Comparator 复核，还换第二套内核又查了一遍。它也写死了那句：结果纯粹是渐近的，对实践中解公式没有任何说明。

还有一句我最想让你看，来自它仓库的 README：Lean checks the proofs, but no machine checks that this file says what the paper says.

翻过来讲：机器验的是这份证明对不对。没人验这份证明，证的是不是你宣称的那件事。

顾问组前一天说过

九月二十一号，OpenAI 公布了一个顾问组，叫 AGMAI。普林斯顿高等研究院 IAS 主办，独立于 OpenAI 运作，成员不接受 OpenAI 报酬。9 个人。Gowers、Hairer、Witten 都在名单里。陶哲轩不在。

10 月 25 日，AGMAI 在陶哲轩博客上发了一篇客座文章，反对 AI 公司指定数学家去领读 AI 产出。结论原话是 on balance the disadvantages outweigh the advantages，弊大于利。其中一条理由几乎能直接搬过来。被选中的数学家，名字最后会替这次发布背书，替公司挡批评。

第二天，OpenAI 对外说的正是请了领读人来组织大家理解结果。数学那项仍然没组，这句落在三人组和五人组上。时间挨得太近，因果我不猜，两件事并排放着。

九月那笔账对一遍

九月我写过两次这类事，两次都留了同一个问题：AI 说它证出来了不算数，那什么算数？当时我给的三样：证明全文公开、独立数学家验过、Clay 认。

前两个有下文：数学和计算机科学的论文、Lean 都公开了，物理一样没有。独立数学家这边，计算机科学有个三人组，公开信里写着参与不等于认证；数学压根没组；物理五人组自己写论文。Clay 那边没动，领奖条件一条都没满足。

方向也挪了：九月五号那次，AI 干的是把人类数学家的证明翻成 Lean。九月九号那次，结果自己产，可证明全文压着不发。这次 Lean 发布前就跑完了，材料放出一部分，再请人来读。

九月那句「编译器说了才算」，改一个字都不够，得补半句：编译器只管它看到的那个陈述。陈述是谁写的，成了新的风险点。

我博客的检查清单里，构建通过、页面能开、字数够数，全是机器能立刻判的。可文末那张知乎回链卡片，没有任何一道检查管它。那批链接用英文地址拼，我这站只认数字文件名。有那么一阵，从知乎点过来的读者，落地是一张 404。我每天看后台，只有「构建成功、字数达标」，一个红字都没有。直到有天自己点了一次那张卡片。检查验的是它看得见的那一段，我关心的是另一段。

所以「OpenAI 学会先验再发了」这个说法，我只认一半。顺序确实反了：先把 Lean 跑完，再发公告。可它先验的，是机器能验的那一半。剩下一半，有的当原料放出来，有的压着不发。这不叫同行评议。

下次看到先看三样

以后再刷到「AI 证明了 X」，可以先看三样。

头一样，论文原文在不在。找不到论文，后面都不用看。

接着看 Lean 仓库，看它验的是哪一条陈述。最好翻一眼那种逐条对照表，看 Lean 形式和论文原句差在哪。两边对不上的地方，才是你要看的地方。

还剩一样，验证的人是谁，他有没有公开说「这不是认证」。

三样看完，手里就有档位了：全在，是能细读的结果。记得问一句，那组人有没有说「这不是认证」。论文和 Lean 在、没人组队，是能读但没人陪读的原料。论文都不在，那就只是一条公告。

标题那句「都说 AI 证了三大难题」，现在可以改得更准。AI 确实给出了三份结果，只是被验到的深度差着三档。

机器能验的那一层，这次确实往前推了一大步。它验不到的那一层，还得有人去读，去问一句，这算不算认证。

这套看法我先给自己留着。等下一条「AI 证明了」刷过来，翻出来对一遍。你要是也用得上，点个收藏。

你下次看到这类消息，第一眼会去翻论文原文、翻 Lean 仓库，还是先看发这条的人是谁？评论区聊聊。