OpenAI 称其 AI 推翻指数时间假设，Lean 证明与运行时间解读

解释 · 2026年10月27日，星期二 OpenAI关于指数时间假说为假的主张，解释：ETH说了什么，算法实际有多快，以及Lean证明检查了什么 2026年10月26日，OpenAI表示其模型产生了三项成果，其中包括一种反驳指数时间假说的算法。本页用通俗语言解释该假说，将声称的运行时间换算成数字，并解读Lean定理，以说明它确定了什么、没有确定什么。 一分钟速览 - OpenAI表示，其未发布的模型产生了三项成果：ETH为假；局部光滑猜想在所有维度上成立（这解决了Kakeya问题）；QCD作为严格的量子场论存在。 - ETH曾表示，3-SAT所需时间按2的n的某个固定分数次方增长。该论文给出了一种确定性算法，能在多项式空间内以快于该速度计数每一个解。 - 增益增长非常缓慢。将隐藏常数设为1时，一般界只有超过约5.4亿个变量时才能胜过当今最好的3-SAT算法。真实常数并未给出。 - Lean定理证明的是一个更弱的界。即使常数取1，它也只有在n约有2,400位十进制数字时才能胜过朴素的2的n次方。它解决的是数学问题，不是任何实际问题。 - 由Russell Impagliazzo、Ramamohan Paturi和Ryan Williams领导的工作组将审查该证明。其中两人提出了ETH。 OpenAI宣布了什么 2026年10月26日，OpenAI宣布了数学、计算机科学和物理学领域的三项成果，由内部模型产生。它称这些手稿为“原始研究数据”，并请外部专家分别担任每项成果的指导人。 - 数学：证明了Sogge 1991年局部光滑猜想在所有维度上成立，OpenAI称这也解决了所有维度上的Kakeya猜想和Stein限制猜想。AI输出于10月18日产生，次日用Lean形式化。两者均已公开。 - 计算机科学：证明了指数时间假说为假。AI于10月16日发现该证明，并于10月17日用Lean形式化。证明和Lean文件均已公开，由Russell Impagliazzo和Ramamohan Paturi（加州大学圣地亚哥分校）以及Ryan Williams（麻省理工学院）领导的工作组将验证并解释它。 - 物理学：包括QCD和标准模型完成在内的量子场论存在性证明，其中包含纯Yang-Mills理论。由2004年诺贝尔物理学奖共同得主David Gross领导的工作组将撰写论文，AI产物未发布。OpenAI表示Yang-Mills的Lean形式化于10月16日完成。 OpenAI表示不寻求学术荣誉，工作组无报酬且可自由发表，并将资助一场关于ETH成果的会议。它还指出已向西蒙斯基金会捐款500万美元，用于举办关于AI产生成果的研讨会。 3-SAT问的是，你能否为n个真或假变量赋值，使得每个由三个变量组成的子句都得到满足。尝试每一种赋值需要2的n次方步。 更聪明的方法表现更好，但只是在指数上相差一个常数因子。论文列出了Schoning局部搜索算法的(4/3)的n次方，以及Jiang和Cai最近一篇预印本中约1.307的n次方。 Impagliazzo和Paturi与Francis Zane一起提出了ETH。论文引用了他们2001年的工作。该工作称，3-SAT在最坏情况下需要2的（n的某个固定分数）次方。任何技巧都无法使该分数缩小到零。OpenAI的帖子称，ETH已被数百篇论文用于证明其他问题是困难的。 强ETH是比ETH更强的主张，因此如果ETH为假，强ETH也随之倒下。P与NP未受影响：论文本身指出，在一般归约下，此类界不会推广到所有NP问题。 论文声称了什么 该论文日期为10月17日，10月25日修订，给出了一种确定性算法，对每个固定的k（k为2或更大），使用多项式空间计数k-CNF公式的每一个满足赋值。 - 一般公式：时间(n + m)的固定次方，乘以2的O(n乘以ln ln n的平方根除以ln n)次方。 - 至多D乘以n个子句的公式：2的O(n除以ln n的平方根)次方。 计数比判定更难，因此同一算法可判定3-SAT，并可逐个变量找到解。论文还推导出更快的图着色、独立集和完美匹配精确计数，以及一个新的电路下界。 用数字表示它有多快 大O记号隐藏了常数，论文未给出这些常数。因此下表将每个隐藏常数设为1。这是我们的假设，真实常数可能大得多： Exponent per variable (bits of work per variable), with every hidden constant set to 1 n (variables) general bound sparse bound Lean statement PPSZ (best known) 1,000 0.53 0.38 1.42 0.386 1,000,000 0.44 0.27 1.86 0.386 1,000,000,000 0.38 0.22 2.02 0.386 general bound = sqrt(ln ln n / ln n) paper, Theorem 1.1, any clause count sparse bound = 1 / sqrt(ln n) paper, Theorem 1.1, clauses <= D times n Lean statement = (ln ln n)^2 / sqrt(ln n) the weaker bound the Lean theorem proves PPSZ = log2(1.307031578) Jiang and Cai's randomized 3-SAT bound, cited in the paper 这样读表。已知最好的3-SAT算法每个变量约需0.386比特的工作量。新的一般界只有到约5.4亿个变量时才能低于该值，即使常数取1。稀疏界覆盖每个变量子句数固定的公式，在常数取1时约在800个变量处低于该值。 这就是为什么OpenAI自己的帖子说，将其转化为实际改进“将需要大量进一步研究”。该结果关乎成本在无穷远处如何增长，而不是你今天运行的任何求解器。 Lean证明检查了什么 该仓库提供了一个Comparator挑战、一个用普通Lean陈述该定理的简短Lean文件，以及一个证明它的独立解决方案库。陈述exact_count_and_sat说：对于每个k（k为2或更大），存在一台多带机和正常数C、A、S、d和e，使得对每个k-CNF公式，该机器在C乘以（输入比特数+1）的d次方，乘以2的A乘以rho(n)次方步内停机，给出精确计数和正确的是或否答案，并使用多项式空间。 这里rho(n)是n乘以(ln ln (n+16))的平方除以ln (n+16)的平方根。论文称其为较弱的指数，来自其第6.4节。从长期看，它仍小于n的任何固定分数，因此它确实反驳了ETH。 两个限制很重要： - 常数只是说存在。陈述从未命名它们，因此证明没有给出可用于真实公式的可计算界。 - rho(n)除以n只有在ln n超过约5,500时才降到1以下，这意味着n约有2,400位十进制数字。低于该值时，即使常数取1，已证明的界也比尝试每一种赋值更差。 该挑战只允许使用Lean的三条标准公理。根据GitHub 10月27日的文件列表，解决方案文件夹包含3，977个文件，约35.5 MB。我们并未自行构建它。README给出了命令：lake env comparator ComparatorChallenges/SubexponentialSAT.json。 来自代码库的背景 - openai/math代码库收录了373个家族的721份手稿。其README称，约42%的顶级结果已在Lean中形式化。 - 在向模型提出的约4，000个问题中，每个结果平均使用了三小时的ChatGPT Pro思考计算。 - 10月7日，OpenAI因一个符号错误破坏了论证而撤回了三份手稿，并修订了另外14份。未经Lean检查的结果可能是错误的，README也说明了这一点。 受影响者 案例 状态 假设ETH的复杂性理论论文 通过假设ETH证明的硬度结果，如果反驳成立，将失去这一支持。工作组正在核查。 强ETH及基于它的结果 SETH蕴含ETH，因此如果证明成立，SETH也随之倒下。 SAT求解器及使用它们的工具 目前没有变化。收益只在远超真实输入的规模上出现，且常数未说明。 P versus NP 据论文本身所述，未受影响。 该做什么 - 阅读Sources下列出的Lean挑战陈述。它约220行，是证明所检查的确切主张。 - 如果你从事复杂性研究，请关注Impagliazzo、Paturi和Williams工作组，该工作组邀请社区参与公开审查。 - 不要基于这一结果更改任何求解器、安全估计或产品计划。 - 将未经Lean检查的AI生成证明视为草稿。10月7日的撤回说明了原因。 仍未知的事项 - 证明是否站得住脚。工作组的验证才刚刚开始，他们的参与并不代表认可。 - Lean陈述是否与预期主张完全一致。Lean检查证明的是所写陈述，因此专家仍需确认它说的就是ETH所涉及的内容。我们阅读过并认为确实如此，但这是我们的解读。 - 隐藏常数的大小，论文和Lean陈述均未指明。 - 物理材料未公开，因此Gross小组之外目前无人能核查QCD主张。 - 表格中的数字假设常数为1。它们展示的是界限如何增长，而非实际运行时间。 来源 - OpenAI，“与学术社区合作构建科学理解”（2026年10月26日）——原始报告 - OpenAI，“指数时间假说为假”（预印本，2026年10月25日修订） - OpenAI，次指数SAT结果的Lean挑战陈述 - OpenAI数学代码库README（721份手稿，结果如何产生） - OpenAI数学代码库历史（10月7日撤回，10月26日新增） - The Decoder，“OpenAI邀请包括诺贝尔奖得主在内的外部专家检查其AI生成的证明”（2026年10月27日） 今日完整版：AI News Report · 每天早晨，每条头条。