ETH 是關於可滿足性問題本質難度的猜想：概括而言，它主張 k-SAT（k ≥ 3）無法在 2o(n) 時間內解決，其中 n 是變數數量；換句話說，不存在能在所有實例上，於 n 的次指數時間內執行的演算法。實際上，ETH 為困難度提供了基準：許多關於圖問題、資料庫查詢與計算生物學的條件式下界，都假設 ETH 成立，藉此指出若要突破特定執行時間，將是令人意外的重大進展。研究人員稱某個問題具有 ETH 困難度，意思是任何大幅改善都意味著必須突破這項基準。

OpenAI 的主張針對固定寬度 SAT：這類 SAT 實例受限於子句結構或變數之間的互動方式。若有人建構出一種演算法，能在 2o(n) 時間內（即 n 的次指數時間）解決所有固定寬度 SAT 實例，就會與 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 公司與學界合作的一種正向模式。

這起事件展現了一種新的研究流程：生成式模型可以提出猜想，甚至產生可供機器驗證的證明，縮短從構想到形式化成果的時間。對研究團隊、資助者與產品領導者等利害關係人而言，眼前的行動方向是投入驗證基礎設施、建立開放的成果儲存庫，並資助由社群推動的稽核工作。風險依然存在：模型可能產生錯誤引理，卻仍通過型別檢查；也可能誤用定義，或利用狹窄的實例假設。正確的應對方式既不是盲目炒作，也不是一概否定，而是由領域專家主導，進行有架構且透明的驗證。