ETH是关于可满足性问题内在难度的一项猜想。粗略地说，它认为k-SAT（k ≥ 3）无法在2^o(n)时间内求解，其中n是变量数量；也就是说，不存在一种算法能对所有实例都在关于n的次指数时间内完成求解。在实践中，ETH为问题难度提供了基准：许多关于图问题、数据库查询和计算生物学归约的条件下界，都以ETH为前提，来说明要突破某些运行时间将是非同寻常的进展。研究人员称某个问题是ETH困难的，意思是大幅改进算法将意味着突破这一基准。

OpenAI的主张针对固定宽度SAT：这类SAT实例受到子句结构或变量间相互作用的限制。如果有人构造出一种算法，能在2^o(n)时间内求解所有固定宽度SAT实例（即关于n的次指数时间），就会与ETH对k-SAT问题族所作的普遍指数级下界断言相矛盾。这将推翻许多明确以ETH为前提的条件困难性结果。关键在于，推翻ETH并不等于证明P = NP：ETH是一个更强、范围更具体的猜想，关注运行时间对指数项的精确依赖。P = NP意味着多项式时间与非确定性多项式时间之间的差距消失；而某个特定SAT问题族存在次指数算法，只能说明该问题族的渐近运行时间更快，并未声称所有NP问题都能在多项式时间内求解。

用Lean对证明进行形式化是重要的一步：它要求定义精确无误，弥补许多非形式论证中的漏洞，并生成可由机器核查的产物，从而避免某些类型的人为错误。OpenAI团队称，自然语言反证提出后不到24小时，Lean形式化便已完成。不过，形式化验证确认的是证明相对于形式公理和定义在语法层面上的正确性；它不能取代学界对模型假设、渐近分析中的隐藏常数、参数范围，以及算法究竟适用广泛还是只针对病态实例族等问题的共同解读。

OpenAI邀请了一个由Russell Impagliazzo、Ramamohan Paturi（ETH最初的两位提出者）以及MIT的Ryan Williams领衔的审查小组。这三位专家兼具相关历史背景和深厚的技术权威：Impagliazzo和Paturi能够判断候选反证是否真正与ETH的原始表述相矛盾，Williams则可评估其对算法下界及相关条件结论的影响。他们的监督有助于以透明、专业的方式对这一研究成果进行梳理，也体现了AI公司与学术界开展建设性合作的一种模式。

这一事件展现了一种新的研究流程：生成式模型可以提出猜想，甚至生成可由机器核查的证明，从而缩短从创意到形式化成果的周期。对研究团队、资助方和产品负责人等相关方而言，当务之急是投资验证基础设施、开放的研究成果存储库，以及有经费支持的社区审查。风险依然存在：模型可能编造错误引理，但这些引理仍能通过类型检查；也可能误用定义，或利用狭窄的实例假设。正确的应对既不是盲目炒作，也不是本能否定，而是由领域专家主导、以结构化且透明的方式进行验证。