AI 推翻了 27 年的「指数时间假设」，机器验证全过了——但有一页没人读得懂
一句话先说结论：10 月 26 日 OpenAI 宣布，其内部模型证伪了理论计算机科学里支撑了 27 年的「指数时间假设」（ETH），证明还通过了 Lean 机器验证。B 站 UP 主 T8star-Aix 在 10 月 30 日发的这期视频里做了一件更较真的事：他把 Anthropic 那份 Lean 工程下载下来，在自己电脑上从头编译了一遍，18 分 40 秒编译通过——然后发现整件事真正的难点不在数学，而在「谁来证明这份证明是对的」。
先讲结论：这次被推翻的不是一道题，是一整层地基
ETH 说的是：3-SAT 这类问题，不存在真正意义上的亚指数时间算法，你只能把指数底数压小，但那个「乘法」永远甩不掉。
这不是某个冷门猜想。过去二十多年，图论、组合优化、数据库查询、计算生物学、计算几何里几百篇论文的「条件性下界」，都是拿 ETH 当地基写出来的——「在 ETH 成立的前提下，这个问题的复杂度下界是 X」。地基一旦被抽掉，这些结论全部要重新审视。
而这次给反证的，是 AI。OpenAI 说它的模型在 10 月 16 日生成了自然语言证明，10 月 17 日完成 Lean 形式化验证；几乎同一时间，Anthropic 也宣布 Claude 在同一天独立找到了类似结果，还专门注明「与 OpenAI 的结果独立且并发」。两家用完全不同的数学工具，撞上了同一个答案。
视频里那面「开关墙」，是三分钟讲懂 ETH 的最好方式
作者用一个开关墙的比喻把 3-SAT 讲清了：
墙上有一排开关，旁边一叠小纸条，每张纸条写着三个开关，比如「3 号开」「7 号关」「12 号开」。规则是每张纸条只需要三个条件里满足一个，问题只有一个——有没有一种开法，让所有纸条同时通过。
这就是 3-SAT。看着像小游戏，但很多硬问题最后都能翻译成这面墙：线路验证、排班、约束求解。最笨的办法就是一个个试，作者在自己电脑上真跑了：
- 20 个开关：0.03 秒
- 25 个开关：0.9 秒
- 30 个开关：22.7 秒
- 31 个开关：44.7 秒
规律很清楚：每多一个开关，耗时差不多翻一倍。照这个斜率，60 个开关要跑 700 多年。
1999 年，Russell Impagliazzo、Ramamohan Paturi 和 Francis Zane 把这件事写成了一条假设：底数你可以压小，二十多年里最好的算法已经能把「每次翻倍」压成「每次乘 1.3」——但那个「乘」永远甩不掉。这就是 ETH。
三件被误读的事：不是 P=NP，密码学也没完蛋
视频里直接点了三个最常见的误读，答案是「一个都不对」：
- 不是 P=NP。证伪 ETH 只说明存在亚指数算法，离多项式时间还差很远。P vs NP 的大门没被推开。
- 密码学不会因此崩。现在的密码本来就不建立在 ETH 上。
- 跟以太坊没关系。ETH 这个缩写撞车了而已，弹幕里真有人问以太坊是不是要跌。
为什么不威胁密码学？作者把关键数字摊开了：Anthropic 论文第二页写着，新算法要在某个规模之上才比原来的算法快——那个规模是 10 的「1 亿次方」量级。注意，不是 1 亿个开关，而是一个有 1 亿位的数字。光把这个数写出来要印三万多页；作为对比，整个可观测宇宙的原子总数写出来才 81 位。
所以这面墙，宇宙都装不下。
那到底推翻了什么？推翻了「惩罚甩不掉」这句话本身。作者打的比方是：有人证明了，只要跑道比宇宙还长，就存在一种更快的跑法。
最戏剧性的一幕：提假设的人，被请来审查推翻它的人
OpenAI 没有自己给自己发认证。它请了一个外部小组牵头，成员是 Impagliazzo、Paturi 和 MIT 的 Ryan Williams——前两位正是 ETH 的提出者，Williams 则证明过 ETH 的一些强化版本不成立。
这个小组在公开信里先说了一句很重要的话：「我们参与，不代表我们认证。」
OpenAI 还答应了两件事：公开全部原始数据供社区独立验证，以及出资办一场学术会议讨论这件事对整个领域的冲击。自然语言证明和 Lean 证明都已经挂在 openai/math 仓库里。
作者对这段的评价挺到位：达尔文和华莱士几乎同时发现自然选择，牛顿和莱布尼茨几乎同时发明微积分——两家 AI 在同一天、用不同工具撞上同一个答案，本身就说明「这个结果可能真的到了」。
他真跑了那份证明：18 分 40 秒，卡在一页没人读得懂的地方
这是整期视频最有价值的部分，也是大部分转述里没有的。
OpenAI 那份代码体量太大，官方自己都建议拆开一块块编译。所以作者选的是 Anthropic 那份，10 月 29 日早上拉下来，从头编译。
跑到第三分钟，屏幕上跳出两条黄色警告。凑近看，是题面文件（spec）报的——意思是「这里空着，需要人来填」。而这块空着的地方，是整份证明里唯一一处必须由人亲眼看过的部分。
等了 18 分 40 秒，编译成功。最后两行翻译成人话就是：除了题面，证明里一个空洞都没有。
但作者紧接着说了句关键的：这不算数。
机器验证管不到的那件事：题面对不对
他举的例子很日常：你让 AI 写个打折函数，它把「打八折」写成了「减八块」；你再让它写测试，它也照着「减八块」来写。一跑，全绿。
Lean 就是那个测试。它能保证「证明和题面对得上」，但题面本身写没写对，它管不了。
这套证明有 1000 多个文件，机器全查完了。真正需要人读懂的，是题面背后的 128 个定义文件，再加一步标准换算，182 行。作者说自己大部分看不懂，但有一行认出来了——「存在一种开法，让每张纸条至少满足一条」。就是开头那面开关墙。
剩下的他丢给 Claude，让人话讲一遍。Claude 讲得挺明白，但当他追问「这里会不会写错」时，Claude 想了一分多钟，列了九个可能作弊的口子，结论是「都读上了」，同时老实交代：从机器换成普通电脑那一步没写进 Lean，靠的是文字论证。
这不是孤例。视频里提了一个前例：9 月 8 日 OpenAI 说解决了千禧年难题之一的 Navier–Stokes 方程，附了 Lean 证明；不到一个月，有人发论文，标题叫《迷失在翻译中》——意思是 Lean 里正义的那个命题，跟论文里说的根本不是同一个。OpenAI 后来也承认确实有差异。
编译过了，翻译却可能是错的。这就是题面为什么只能靠人读。
那这 182 行，到底谁检查过？
Anthropic 在论文里自己交代了：这些 Lean 代码是 AI 写的，再由同一批模型的其他实例来审；写论文那会儿，还没有已知的人类检查过。
作者那句自嘲很真实：「我刚才那一遍，说白了就是让一个 AI 去审另一个 AI 写的东西。」他还补了一句可能戳到很多开发者的话——AI 写完代码、测试全绿就直接合并，你干过没有？
数学家那边的真实反应
视频后半段换到了人的一侧，信息密度很高：
- 10 月 6 日 OpenAI 一口气放出 700 多份数学手稿，一位博士生翻着翻着，发现自己正在研究的课题被解决了，基金申请要重写。
- 王虹和合作者证明三维挂谷猜想写了 127 页，数学界读了一年多，她因此拿了菲尔兹奖；而 10 月 26 日 OpenAI 说把这个结果推到了任意维度——到 10 月 29 日，还没有专家公开说它对不对。
- 菲尔兹奖得主抱怨，自己公开提过的那些大问题全被宣称证明了。陶哲轩的比喻是：像看电视剧被剧透了，就没法假装没听过。更深的担心是，以后年轻人不想研究数学了。
- 丘成桐的态度相反：海啸已经来了，与其躲着，不如在浪上冲浪。
不管站哪边，大家撞上的是同一堵墙：证明写得越来越快，人读得还是那么慢。 读不过来，最后只能让 AI 去审 AI。
所以 AI 到底赢没赢
作者的判断很克制：审查组还没给结论，也还没人报告发现错误，他们打算年底前开线上讨论会。他自己的押注是「它真的成立」，并且承诺如果年底讨论会真发现错误，就专门再出一期。
但他给出了一个比结论更耐用的东西——审核 AI 发现的三个动作，这也是普通人现在就能用的部分：
- 先让它用人话把题目复述一遍。如果它复述出来的问题和你以为的不是同一个，后面全白搭。
- 再看它测试里的断言。测试绿不绿是结果，断言写的是什么才是前提。
- 最后才看是否全绿通过。顺序反过来，你会被「全绿」骗过去。
适用与不适用
这篇内容对谁有用：
- 关心大模型推理能力边界、想知道「AI 做科研」现在到哪一步的人；
- 要把 Lean / 形式化验证接进自己工作流的工程团队——它能验证什么、不能验证什么，这里有具体案例；
- 需要向别人解释「为什么机器验证通过还不算定论」的人，可以直接用打折函数那个类比。
哪些情况别照搬：
- 别把「Lean 编译通过」当成「数学结论成立」。它只证明证明与题面一致，题面的正确性仍要人读。
- 别把它读成 P=NP 或密码学危机。规模门槛是 10 的 1 亿次方位，物理上不可达。
- 别现在就当定论引用。截至 10 月 29 日，外部审查组尚未公开结论，也没有专家公开确认或报错。
- 别指望立刻有工程收益。理论上的亚指数算法要变成能跑的代码，中间还有大量工作。
一句话收尾
这期视频最值得记住的不是「AI 又解了个大问题」，而是它顺手暴露的新瓶颈：答案变得越来越便宜，判断一个答案对不对，变得越来越贵。
每多一个开关，时间还是差不多翻一倍。只不过现在我们知道了，在一个谁也到不了的地方，这面墙上有一道缝。
---
来源范围说明：本文主体依据该视频的本地语音转写（Whisper large-v3-turbo 整段转写，术语已人工校对），交叉核对 OpenAI 官方公告、IT之家与 ic.work 的报道。文中涉及的编译耗时、警告内容、182 行题面等细节来自视频作者的实测叙述，非本文独立复现。