大模型证伪 ETH：证书可信，意义存疑-平芜编程栈

它可能推翻了一个统治理论计算机科学领域二十七年的猜想——但没人读得懂它写了什么。2026 年 10 月，OpenAI 与 Anthropic 几乎同日宣称旗下模型在指数时间假设（ETH）上取得结果，前者更一次性放出 372 个前沿问题的预印本。欢呼与警报同时响彻 X 时间线。这篇文章不讨论“AI 是否取代数学家”这类宏大叙事，只把三个问题钉死在一个个技术细节上：证明确实可信吗？从生成机制看它意味着什么？以及——它到底有“意义”吗？

一、背景：被搅动的是什么

指数时间假设（ETH）由 Impagliazzo 与 Paturi 于 1999 年提出，核心主张是 3SAT 不存在亚指数时间算法。它是过去二十余年大量条件性复杂性下界研究的前提：图论、参数化算法、组合优化里成批的"在 ETH 下，问题 X 无法做到 O(…)"的结论，都建立在它之上。

所以一旦 ETH 被推翻，震动的不是一条孤立猜想，而是一整片以它为地基的条件性结论需要重新评估。这里有一个必须说清的边界：ETH 被推翻并不蕴含 P = NP。两者地位不同，混为一谈是这类报道最常见的错误。

另一个容易被忽略的事实："ETH 被证伪"是 Anthropic 侧的声明（Claude 独立完成、约 1400 万输出 token、声称零人类输入）；而"372 篇大礼包 + Lean 证书"是OpenAI 侧的事件。这是两件不同的事，可信度不能混算。

二、第一层追问：Lean 形式化 = 证明严格等价于原猜想吗？

结论先行：不能确认严格等价。从公开材料看，大概率不是"字面等价"，而是“可归约等价”——而那条归约很可能没被形式化。

"有 Lean 证书并通过机器检验"只保证一件事：证明项⊢ statement成立。它完全不保证statement与 Impagliazzo–Paturi 的原始表述是同一个命题。这两件事必须分开评估。

2.1 偏差最常出在哪三处

维度	原始 ETH 表述	常见的形式化漂移
计算模型	多带图灵机（`DTIME`）	算法论文惯例用 RAM / word-RAM，二者间只有多项式开销——但这需要论证，而非默认
参数 n 的所指	变量数	被偷换成子句数 / 公式总长度；`2^{O(n/√log n)}`只有 n = 变量数时才是`2^{o(n)}`
变体选择	标准 ETH	稀疏版 / SETH / bounded-width CNF 等强弱变体，直接决定结论强度

2.2 真正被形式化的，几乎肯定是"正向命题"

几乎可以肯定，Lean 里检验的是一个正向算法命题：

存在确定性算法 A，对 n 变量的 3-CNF 在2^{O(n/√log n)}内判定（Anthropic 侧为更难的计数版 #3-SAT）。

而“ETH 为假”不是一个能直接写成有限证明目标的命题——它要对所有算法量化。通常只能靠"给出一个反例算法"来表达。

从“算法命题”到“ETH 为假”，中间隔着一层标准但未形式化的桥：Impagliazzo–Paturi–Zane 的 Sparsification Lemma（任意 3-CNF 可写成至多2^{εn}个线性子句实例的 OR）。论证是：取ε = δ/2，总时间2^{δn/2 + O(n/√log n)} ≤ 2^{δn}（大 n），对任意 δ 成立 ⇒ 落进2^{o(n)}。

数学上成立，但这条归约大概率没有被一并写进 Lean。也就是说：机器检验的是"算法 + 运行时间 + 正确性"，而“⇒ ETH 假”是论文正文里的元论证。

2.3 一个刺眼的细节

Anthropic 公开摘要里的关键运行时间界是“runs in time ___”——被涂掉了。在看不到被形式化的确切界之前，无法判断它形式化的到底是2^{O(n/√log n)}、2^{O(n/log n)}还是别的量级。

连中文报道自己都点出了这一点：“即使有 Lean 形式化，学术界仍需要弄清形式化定理是否准确对应原来的猜想。”

2.4 判定方法

要回答“是否严格等价”，唯一可靠的做法是逐字比对 Lean 源文件里statement的量化结构与模型假设：

Lean 定理的精确陈述是什么？
用的是什么计算模型？runtime 谓词与论文声称的模型是否一致？
n 的定义是变量数吗？
复杂度界的常数是多少？
Sparsification 桥是否纳入形式化？

在此之前，应标记为“无法判断”，而不是默认成立。

三、第二层追问：这类证明的可信度有多高？

核心判断："大模型证明了 X"这句话本身不构成可信度证据。决定可信度的，是证明以什么形式交付、被验证到哪一步。按此标准，至少分三档，差别极大。

3.1 可信度三档

第一档：有 Lean 证书（机器检验）——最强，但有明确边界

边界一：Lean 只保证"证明项成立"，不保证陈述忠实对应原始猜想（详见第二节）。
边界二：可验证 ≠ 可理解。UGC 有 Lean 证书，但据 Dana Moshkovitz 评价，论文写得“像嗑药的人写的”“引用常常无关且混乱”——机器能验，人读不懂。这是两种不同的可信度。

第二档：只有自然语言论文，无形式化——未验证状态

最有力的反例就在眼前：OpenAI 那批里关于Hodge 猜想的预印本已被撤回，原因是符号错误（sign error）。一个能被外部一眼挑出的符号错误，说明这批产出里确实混有实质错误，而非"只是难读"。
底噪数字要计入先验：模型被喂约 4000 个长期未解问题，单次约 3 小时，成功率约 10%——九成是失败的。

第三档：只有 PR 摘要与 X 帖子——待核实的声明

就是媒体报道所处的层级：关键量被涂掉，无预印本细节，无第三方意见。

3.2 这次 ETH 的位置

比一般传闻好一些：OpenAI 侧已请Impagliazzo、Paturi、Ryan Williams组织外部审计——这三人正是 ETH 的提出者与核心研究者，让他们审“形式化陈述是否忠实对应原猜想”，是对口的。但审计尚未出结论。官方顾问组措辞很克制：明确说“既不背书也不否定，评估只能由数学界自己完成”——这个措辞本身就是对“可信度尚未确立”的官方确认。

3.3 分层结论

"存在亚指数 3SAT 算法"这一正向命题：若有 Lean 证书且审计确认陈述无误，可信度高。
"ETH 被证伪"这一推论：可信度中，取决于未形式化的归约是否被补上。
“AI 独立成为论文唯一作者”：无法判断——"零人类输入"的操作定义、脚手架与筛选由谁做，公开信息不足。
“372 项结果整体可信”：不应默认。已有撤回先例、多数无形式化、无人读懂，正确姿态是逐篇对待。

一个可操作的判据：看有没有 Lean 证书 → 看形式化陈述是否等价于原猜想 → 看是否有人能独立复述证明思路。三者缺一，可信度就掉一档。

四、第三层追问：从生成原理看，是"猴子打出莎士比亚"吗？

一个流行的判断是：LLM 是概率采样，所以它的“证明”本质是低概率命中，没有实质性突破。把这个判断拆成两个独立命题，会发现真假不同。

命题 A（机制）：LLM 是概率采样，产出是"低概率命中"而非理解。
命题 B（实质）：真正的突破必须是"把方法（继承的或自创的）用到前沿难题上"。

问题在于A 推不出 B。就算 A 完全成立，也只能说明“产出过程是搜索”，不能说明“产出物没有方法”。而命题 B 其实是一个后验的、看输出结构的标准——不看生成机制，看这个定理能不能压缩成一个可迁移的方法。用“LLM 原理”去做先验否定，逻辑上不成立。

4.1 "猴子"类比在大学问上不成立

无限猴子定理的前提是均匀随机：字母表上等概率、无目标信息、靠无穷时间凑出概率 1。LLM 不是这个。它是"经过数学语料训练的先验分布 + 采样 + 外部验证器（Lean）“的generate-and-test 管线：1400 万 token、约 3 小时、10% 成功率——这不是"均匀乱打”，这是massively parallel biased sampling + verifier filter。AlphaProof / AlphaGeometry 同属这一范式，在 IMO 上是真出过结果的。

但这里有一个对批评者有利的反转：那个"先验"不是模型自己的，是人类数学文本压缩出来的分布。proposal distribution 的熵来自人类方法库——所以"方法"确实是继承的，模型贡献的是"在该分布下的高维采样"。这恰好对应"没有自创方法"的直觉，只是论证路径要反过来：不是因为"随机"所以没方法，而是因为"proposal 来自人类语料"所以方法多半是借来的。

4.2 软件视角：证书有效 ≠ 生产者聪明

这是最该讲清楚的一层。Lean 给的是一个certificate：验证是多项式时间的，生成是搜索。验证器只能判断“这个证明项是否⊢ statement”，它在结构上无法区分“天才构造”和“运气命中”。

证明可信（certificate 有效）与突破实质（方法可迁移）是正交的两件事。

Lean 让前者成立，但一点都不蕴含后者。一个 lottery 命中的证书，仍然是真定理。数学是结果主义/验证主义的——它不要求证明者“懂”。

4.3 真正的不对称不是"运气"，是"可解释性"

人类前沿数学也大量依赖启发式搜索与偶然——Ramanujan、Poincaré 的“灵光”、Gauss“先有结果后补方法”。人类与当前 LLM 的真正不对称不是“有运气 vs 没运气”，而是方法的可解释性与可迁移性：

找到证明的人类通常能解释、泛化、教学、调试；
模型给不出搜索路径，问它为什么对，得到的是事后合理化而非真实推理链。

要批的应该是这一点——它真实而致命；“随机”不是。

还有一个分配问题：这次“理解”被外包给了验证共同体（Impagliazzo 等外部审计）。那么到底算"AI 做出了突破"，还是"AI 当了个幸运 oracle、人类完成了理解"？这本身就有争议，而且更接近批评者的立场。

4.4 一个关键的经验问题

按“自创方法”这个标准，突破与否是要经验核实的，不能从机制推出。真正可操作的判据是压缩性与泛化性（一个香农式/最小编码问题）：

若那个 3SAT 构造能压缩成一段短的、可复用的技术，并迁移到别的参数化问题 → 按定义它就是突破，不管怎么被采样出来。
若它只是对这一个实例生效的 ad-hoc gadget、不可复述、不可迁移 → 就更接近“命中”。

当前证据是混杂的：符号错误撤回、9/10 失败、UGC“机器能验人读不懂”——支持“看到的是筛子不是脑子”；但 10% 成功率本身两头不讨好：真理解者不该失败 90%，纯运气者该失败 99%+。10% 恰好落在“强模式匹配、弱理解”的区间。目前无法判断构造是否可迁移，因为没人复述得出核心思路。

五、“AI 的证明没有意义”——这句话过强

"意义"不是数学对象的属性，而是人对它的使用关系。把它当成客观结论来讲，是这句话最大的问题。

5.1 把"意义"拆成五种

一个定理的价值可以拆成：

确立真值——把命题从 open/猜想变成定理；
解释——说明为什么为真；
迁移——产出可复用的技术，能做下一个问题；
作为引理被消费；
使领域重排——改变下游条件性结论的地位。

"没有意义"成立的最强版本只可能指向(2) 和 (3)。但(1) 和 (5) 不依赖任何人读懂：ETH 若真被推翻，所有以 ETH 为前提的条件性下界必须重新评估——这是客观后果。

而(4) 更是被这次事件直接推翻的假设：如果证明的消费者正在从人变成机器，那"人类读不懂"就不等于"没用"——一个人类读不懂的引理，照样可以是模型的下一个 building block。这一点直接击穿"没有意义"的普遍形式：它默认读者一定是人，而这个前提正在失效。

还有一层没被算进去的：Lean 证书本身就是持久资产。它把"信不信这个证明"从社会学问题降成多项式时间可判定问题，这是真的认识论收益。可验证性有意义，即使可理解性没有。

5.2 历史参照：四色定理与 Flyspeck

四色定理的机器证明当年也被批评为“不是真证明、不启发人”，Flyspeck 形式化了 Kepler 猜想——历史证明这类质疑部分错了，它们最终被接受。但有一个真实差别需要承认：那些是人类设计、机器验证，搜索路径是人的；这次是搜索本身也不透明。这个区别支持批评，但不支持“没有意义”这个全称判断，只支持“解释价值和工具价值目前尚未兑现”。

5.3 从机制推不出"没意义"

"意义"是人对产出物的使用关系，不是对象的属性。所以"AI 原理是采样 ⇒ 证明没意义"这一步不成立——采样机制决定的是生产过程的性质，不决定产出物的用途。同一个不可读的定理，在被当作真值锚点、被机器当作引理复用时，是有意义的；只在"要求它启发人类直觉"这个特定用途下才显得没意义。这是把一个用途维度上的短板说成了对象本身的无价值。

5.4 真正的分歧是价值论，不是事实

这其实是关于**数学的 telos（目的是什么）**的争论，不可能从 LLM 架构里任何地方推出来：

若数学 =真理的收集，那 AI 证明意义很大，而且会越来越大；
若数学 =人类理解的技艺（能解释、能教、能 debug、能迁移），那当前这类不可复述的证明意义很小。

两个立场都正当。但“没有意义”是个全称否定：它要么滑向第一种立场下明显为假，要么偷偷预设第二种立场却当成客观结论来讲。

六、总结：三个判断

“因为 LLM 是随机采样，所以不可能是实质突破”——论证不成立。机制层面的说服力不如想象中强，且与后验定义自相矛盾。真正该批的是"可解释性缺失"，而非"随机性"。
“当前证据更像筛子而不是脑子；即使定理为真，也尚未证明方法可迁移”——这个更强的版本成立。撤回、无人能复述、ad hoc 风险都指向它。
“AI 证明没有意义”——过强。更精确的表述是：当前的 AI 证明，其解释价值和可迁移性未经证实且很可能偏低；但作为真值转移和机器可复用的引理，其价值非零，甚至可能很高。“对人的启发几近于零、对数学共同体的工具价值尚未兑现”——这个版本才站得住。