AI 交了三篇，物理组说先别发

北京时间 10 月 27 日 05:18，openai/math 仓库合入一个提交，标题是「Update math/cs papers, formalizations, and verification data」。十七分钟后，公告出现在 Hacker News；UTC 21:36:56，OpenAI 科学家 Dan Roberts 在 X 上贴出公告正文，公司账号转发。公告页自己只印着「October 26, 2026」，取不到一条机器可读的发布时间12。

代码比公告早一小时落地。这个顺序就是这一期的题目：先上线的是能被下载、被编译、被挑错的东西，后上线的是解释。

公告宣布三件事。谐波分析里，模型证出了 Sogge 的局部光滑猜想，在所有空间维数上成立，由此得到 Kakeya 猜想与 Stein 的球面限制估计。复杂度理论里，指数时间假设（ETH）被否证。量子场论里，给出了包含规范场与费米子的四维相互作用量子场论的严格存在性证明，覆盖 QCD 与标准模型的一个统一完备化2。

三件成果走了三条发布路径，路径由外部专家定。公告的说法是请外部专家当 shepherd，组织小组读懂结果、并建议怎么发布，三组给了三个答案：数学那件按 10 月 6 日的老办法，把模型原文与 Lean 直接放进仓库，解释留给研究者自己做；计算机那件把原文与 Lean 立即公开，同时由 Impagliazzo、Paturi、Williams 领的小组负责解释，OpenAI 另外出钱办一个会；物理那件把发布权交给 David Gross 领的小组，小组决定先扣下模型产出，自己重写。

公告自己写下了这套安排的代价：选择最初的 shepherd，必然影响谁先参与，并造成信息不对称。四条原则里，参与者不签 NDA、不取学术功劳、出力者署名、参与自愿且无薪2。

前一天有人写过相反的结论。 数学与 AI 顾问组（AGMAI）10 月 25 日发过一篇《Disadvantages of Designating Mathematicians for AI Output Releases》，逐条反对「指定数学家」这做法：被指定者先看到材料，等于让一部分人抢跑；决定权从共同体手里被拿走；挑选过程不透明，还会激励数学家去迎合公司的优先级；被指定的名字最后会替这次发布背书，替公司挡掉批评。结论句是「we recommend that AI companies do not adopt this practice for future releases」3。这份建议发布在公告的前一天。AGMAI 的成员里有 Edward Witten——Clay 杨–米尔斯问题陈述的另一位作者，他不在物理组那五个人里。

我去仓库数了一遍。 10 月 6 日首发是 722 篇手稿、372 个结果族；10 月 7 日撤掉三篇，剩 719 篇；10 月 26 日是 721 篇、373 族45。这两周三件「新发现」在目录上只多了两篇稿件、一个新族。仓库里 751 个稿件目录多于 721 篇，因为同一篇稿的旧版本按版本各自留了一个目录；lean/docs 下有 245 份形式化说明6。

逐件对：079 族原本叫「Local smoothing in three dimensions」，装的是 9 月 24 日那篇三维临界情形；10 月 26 日族名改成全维，族里加进 10 月 25 日这篇，所以族号没变、稿件 +1。378 族是新的，页首署 10 月 17 日、10 月 25 日修订，纸面 64 页6。

物理那件在目录里是零。preprints 下 751 个目录、CONTENTS 的 373 个族名、lean/docs 的 245 份说明，逐条查过，没有 Yang–Mills、没有 QCD、没有标准模型条目；连公告说它所依据的 Balaban 构造性量子场论路线，整个仓库也没有一处引用。公告说物理组的 Lean 形式化 10 月 16 日就完成了，这份完成品同样不在公开仓库里。所以「暂不公开模型产出」在执行层的含义是：这篇稿、连同它的形式化，一起没有出现。

千禧年问题只答了一半，另一半没提。 Clay 的题目叫 Yang–Mills Existence and Mass Gap，正式表述是「Prove that for any compact simple gauge group G, a non-trivial quantum Yang–Mills theory exists on R⁴ and has a mass gap Δ > 0」——存在性与质量间隙两条都要7。公告自己的措辞是「As a subproblem, this work also includes a proof of the existence of pure Yang–Mills theory, which is part of the ... Millennium Prize problem」，只报了存在性2。今年 1 月，Michael Douglas 在《Nature Reviews Physics》给这个问题的现状综述里写，质量间隙「It is widely felt that no clear path is known towards proving it」——存在性在推进，质量间隙还没有路8。Douglas 正是物理组五人之一。

Lean 通过是一条线。 仓库的验证分三层。第一层是 Comparator 的挑战文件，六个定理各以 sorry 收尾——那是待证的命题，写在那里是为了让证明方去关闭它，本身不是证明9。第二层是解模块：local smoothing 那套 73 个文件，SubexponentialSAT 那套 3,977 个文件，两处都没有 sorry、没有 axiom 声明、没有 admit；Comparator 的配置只放行 propext、Quot.sound、Classical.choice 三条公理10。第三层是结论对不对，这一层没人做。

Hacker News 上有人把第一层当成了漏洞：一位用户贴出 378.md 后补了一句「by fucking sorry written at the end of the proof」，另一位用户纠正说，那个带 sorry 的文件只是题面，真正的证明散在 Algorithms 目录里、多到 GitHub 都显示不完11。这条误解与纠正，把三层结构演示得比任何摘要都清楚。

形式化还分档次。378.md 自己写明：Lean 证到的是 2 的 O(n(log log n)²/√log n) 次方那一档；论文里的主定理比它强，是 (n+m)^O(1) · 2 的 O(n log log n/√log n) 次方，靠附录 D 的张量缩并；摘要印的是较弱的那一档 2 的 n/(log n)^(1/2+o(1)) 次方1213。弱的那一档已经足以推翻 ETH，所以结论不受影响；说「主定理已形式化」则多走了一步。

仓库自己演过「形式化过关、结论要撤」。 10 月 7 日的更新记录写着：一篇讲 split abelian eightfolds 上 Weil 类代数性的稿子有一处符号错误，让一条 stabilization-trace 消去论证失效，连带两篇依赖它的稿子，一共撤回三篇；另外修订 14 篇，修证明、改陈述、补假设，其中一处是过时引用；还有 13 篇因为引用了被改的稿子而更新。撤回稿的 README 现在留着说明与归档版链接，并加了一句「This withdrawal concerns the proof; it does not assert that the mathematical statement is false」5。日期有两个口径：撤回说明写「Withdrawn on October 6, 2026」，更新记录列在 10 月 7 日。

覆盖率那个 42% 复算不出来。 README 说「The repository has ~42% top-line results formalized」，更新记录 10 月 7 日给的是 300 / 719。但 lean/formalization.yaml 里只有 176 条 sources、208 条 main_results、192 个去重后的 comparator 配置，用哪一组都凑不出 300 或 42%。「顶线结果」这个词在公开文件里没有定义，所以这个百分比只能照抄原句4。

ETH 为假，改变的是另一批论文的地基。 论文给的是确定性算法：对每个固定的 k ≥ 2，精确计数 k-CNF 的满足赋值，时间 (n+m)^O(1) · 2 的 n/(log n)^(1/2+o(1)) 次方，空间为多项式。因为「精确计数是否大于零」就判定可满足性，k = 3 时 3-SAT 有了 2 的 o(n) 次方的确定性算法。论文据此声明否证 ETH、SETH、Gap-ETH 与 NSETH，同时写明白它与正则消解这类受限证明系统的无条件指数下界不冲突13。ETH 被用来推几百条条件性下界，横跨图论、计算生物、数据库、计算几何；这些下界的地基没了。但 2 的 o(n) 次方仍是超多项式，它不给实用快算法，也碰不到 P vs NP。

数学那篇的自述比公告更宽。 论文摘要里，除了 Sogge、Kakeya 与球面限制，还声明解决了 Bochner–Riesz 猜想与 Nikodym 极大猜想、给出 Schrödinger 方程的局部光滑与 Stein 平方函数的 sharp 界；球面、紧抛物面、截断锥的限制估计证到的是猜想范围的内部，不含端点14。公告只提了其中三件。只读公告的人会低估这篇稿的分量，只读摘要的人会高估它被核过的程度——两边都还没有第三方复核。

钱是三方合出的。 Simons Foundation 10 月 15 日的稿子写的是西蒙斯、Anthropic 与 OpenAI 三方合计 1,500 万美元，由基金会管理、开放申请，用来让研究者评估近期 AI 辅助的结果；一项面向 Math+AI 研究所的定向资助 12 月 1 日截止，两家公司另外提供模型与算力15。500 万这个数字只出自 OpenAI 自己的表述，基金会那篇通稿没有拆三方各出多少。Hacker News 上有人按 500 万算了一笔账，说这大约够 5 到 10 个博士生五年；按通稿的口径，那笔钱里有三分之二来自另外两家11。

外部世界的接法与上一轮不同。 10 月 6 日那批，当天有 Scientific American 与纽约时报；这一轮的第一个小时里，只有科技与财经快讯：The Next Web 写对了，用「part of one of the Clay Mathematics Institute's Millennium Prize problems」；中文快讯用「涉及」承接；主流科学口没有动静16。Scott Aaronson 当晚在博客里提了一句，说学生跑进办公室告诉他 OpenAI 的模型否证了 ETH，他复述的界是 exp(n/√log n)，落笔是「the endless buffet continues!」——他承认结果，没有给判断17。

三位 shepherd 自己先划了界。 Impagliazzo、Paturi、Williams 联署了一封给同行的公开信，开头就写「Our involvement should not be taken as certification of the claim.」信里还写，这次审查「without conferring ownership of the effort on a company or a selected group of researchers, including ourselves」——他们先否认自己拥有这次审查18。信末附的组织方案还是进行时：权威发布地址仍指向 OpenAI 的公告页，社区发现目录打算用只读网盘加一张表单。

没核到的部分也写清楚。 三项结果都没有第三方复核，两篇公开的稿都只有 OpenAI 一个署名；我没有跑 lake build，也没有跑 Comparator，只核到源码层面没有 sorry 与 axiom、配置里的公理清单是三条。物理那件的一切技术细节，目前只能引用公告叙述——没有稿、没有 Lean、没有摘要、没有页数。数学那篇的「辅助偏微分方程」是公告的说法，论文自己写的是守恒流、两条辅助时间坐标与一个四元数行列式方程。42% 那个数字复算不出来。

三件事。

一，这一期的新闻不在数学里，在流程里。同一家公司、同一批模型产出，两星期内用了两种发布办法：10 月 6 日一次性全推，10 月 26 日把「发不发」交给三组外部专家，三组给出三个答案。公告把这三种做法并排列出，并承认自己不知道哪种最有用。这是可核的：目录只多了两篇，第三篇连编号都没有。

二，「Lean 通过」是一句需要补完的话。补三个空：验的是哪一档命题、命题是不是你以为的那个、谁跑过。仓库自己的撤稿记录给出了第一个空的答案：形式化锁得住命题与证明的配对，锁不住这一对是不是你要的东西。

三，读到「AI 证明了 X」，先去仓库看一眼原件在不在架上。这次三件成果里，两件能在十分钟内打开、下载、对照，第三件只存在于一段英文散文里——而它恰好是唯一挂着千禧年问题名字的那一件。