在计算机科学里，有些结论被证明是对的，有些被证明是错的，还有一些，大家都相信它是对的，却始终没人能够证明。

“指数时间假设”就属于最后一类。将近三十年来，无数研究者把它当作默认成立的前提，在上面搭建起一座又一座理论大厦。

如今，OpenAI宣布，它的一个内部模型推翻了这个假设。

如果这一结论经得起检验，它将成为人工智能在理论计算机科学领域取得的最引人注目的成果之一。

一个让宇宙原子都不够用的难题

要理解指数时间假设，得先认识一个经典问题：布尔可满足性问题，简称SAT。

想象一个由许多开关组成的逻辑公式，每个开关只能取“真”或“假”。问题是：有没有一种开关组合，能让整个公式成立？

最笨的办法是穷举，把每一种组合都试一遍。这就像面对一把密码锁，只能从零零零开始一个个往上拨。

十个变量，有一千零二十四种组合，计算机眨眼间就能试完。可每多一个变量，组合数量就翻一番。

到了一百个变量，组合的总数已经超过了可观测宇宙中原子的数量。这就是所谓的“指数爆炸”。

SAT问题还有一个特殊身份：它是“NP完全”问题。这意味着，如果能找到快速解决SAT的方法，就能快速解决所有NP完全问题。

几十年来，没人找到比暴力穷举快得多的通用算法，也没人能证明这样的算法不存在。这与一九七一年提出、至今悬而未决的“P与NP”问题紧密相关。

三十年的“默认前提”

上世纪九十年代末，罗素·因帕利亚佐、拉马莫汉·帕图里和弗朗西斯·赞恩提出了指数时间假设。

它的核心意思是：解决SAT问题所需的时间，必然随着变量数量呈指数增长。换句话说，暴力穷举几乎已经是最优解。

这个假设从未被证明，却被学界广泛接受，成了一种公认的“工作假设”。几十年间，无数聪明的头脑尝试寻找更快的算法，都无功而返，这反过来强化了人们对它的信心。

研究者在它的基础上，建立了大量“条件性困难”结论。这类结论的逻辑是：如果指数时间假设成立，那么某某问题就不可能被快速解决。

这些结论遍布图论、计算生物学、数据库和计算几何等众多领域。

比如，在社交网络里寻找一群人人互相认识的小团体，或者在地图上安排最省事的覆盖方案，研究者都曾借助这一假设，论证这些问题没有本质上更快的解法。

它还有一个更强的“升级版”，被用来论证基因序列比对等常见计算难以突破某个速度极限。

打个比方，指数时间假设就像一栋大楼的地基。几百篇论文都把自己的楼层盖在这块地基上，从没想过它会松动。

AI给出反证，正在接受检验

OpenAI表示，它的内部模型用自然语言写出了一份推翻指数时间假设的证明。

这份证明随后被翻译进了一种名为Lean的证明辅助工具。Lean会逐条检查每一步逻辑推理，确保没有漏洞。

不过，Lean只能保证证明确实推出了那条形式化的命题。这条命题是否准确表达了原本的猜想，仍需要人类专家来把关。

更耐人寻味的是验证团队的阵容。据OpenAI介绍，由因帕利亚佐和帕图里领衔，联合麻省理工学院的瑞恩·威廉姆斯，组成了独立验证小组。

也就是说，当年提出这个假设的两位学者，如今亲自来检验它是否真的被推翻了。

需要强调的是，这一结论目前仍在等待独立核实。只有经过同行确认，它才算真正站得住脚。

威廉姆斯已经在社交平台上公开了这一结果给出的大致时间界限，比严格的指数级只快了一点点。

那么，如果反证成立，会带来什么影响？

首先要澄清一个常见误解：SAT问题并不会因此变得容易，“P与NP”问题也依然悬而未决。

指数时间假设说的是“必须指数级地慢”，推翻它，只意味着存在比严格指数级稍快一点的方法，离“快速求解”还差得很远。

真正受冲击的，是那几百个建立在这一假设之上的困难性结论。研究者需要逐一排查，看哪些结论还能找到别的依据，哪些需要重新论证。

从长远看，如果SAT问题的真实复杂度比想象中低，未来也许能催生更快的算法。芯片验证、软件测试、排班调度等实际问题，很多都能归结为SAT问题。

不过，OpenAI也提醒，把理论上的突破变成实用算法，是另一项艰巨的研究任务。

这次发布并非孤立事件。同一天，OpenAI还公布了另外两项由人工智能产生的成果，其中包括对挂谷猜想的证明。

巧合的是，就在同一天，另一家人工智能公司也宣布，自己的模型独立得出了类似结论。两家实验室几乎同时撞上同一道难题，本身就耐人寻味。

此前，OpenAI在十月六日一次性发布了三百多项数学成果，曾引发数学家们的批评，焦点在于这类成果应当如何审核、如何发布。

从这个角度看，指数时间假设的反证，也是一次对审核机制的检验。

人工智能能不能做出真正的数学发现，最终不靠宣传，而要靠一行行经得起推敲的证明，以及数学共同体审慎的判断。