Wes Roth asks whether AI has found a shortcut through a problem computer scientists expected to be exponentially hard. OpenAI says an internal model produced a proof that the Exponential Time Hypothesis (ETH) is false, and has published a manuscript and a Lean formalization. That is a striking research claim. It is not a proof that P equals NP, a working attack on encryption, or a ready-to-use faster solver. The independent examination is still under way.
If the proof survives expert review, it changes a long-used assumption about the asymptotic difficulty of 3-SAT. OpenAI's claimed running time is subexponential, yet still superpolynomial. The immediate work is to understand and check the proof, then ask whether any of its ideas lead to useful algorithms. OpenAI itself says practical improvements would require further research.
Watch Wes Roth's Discussion
Source note, 28 October 2026: Wes's explanations and analogies come from the supplied transcript and video; we did not reproduce the proof or run the Lean project. We checked OpenAI's public claim and the stated formalization bound against its announcement and Lean scope note, and link the manuscript for direct examination. The independent group's letter expressly says its involvement is not certification.
What OpenAI Is Claiming
ETH concerns 3-SAT, a problem about choosing true/false values so that every clause in a logical formula is satisfied. Roughly, ETH says no general algorithm solves arbitrary 3-SAT instances in 2^o(n) time, where n counts variables. A smaller base such as 1.3^n would still be exponential and would not refute ETH. A genuinely subexponential bound would.
OpenAI's 25 October manuscript claims a deterministic algorithm that counts satisfying assignments of fixed-width CNF formulas in subexponential time and polynomial space. Counting can answer whether any assignment exists at all, so its 3-SAT case would refute ETH. The linked Lean note says the formalization checks a slightly weaker bound than the paper's sharpest headline bound, but one still sufficient for the ETH conclusion. That distinction matters when describing what is machine-checked.
What Is Verified, and by Whom?
| Question | What the source supports | Reader check |
|---|---|---|
| Did OpenAI publish the work? | Yes: the math repository contains the paper, proof artifacts and revision history. | Read the ETH entry and track later corrections. |
| Is there a Lean check? | OpenAI reports one; its scope note specifies the bound it formalizes. | Formal checking tests a stated theorem inside its definitions. Experts must still inspect the definitions, paper-to-code match and argument's meaning. |
| Have independent experts signed off? | No certification is claimed by the Impagliazzo-Paturi-Williams review group. | Follow its public examination rather than treating participation as endorsement. |
| Is there a useful new solver? | OpenAI says practical algorithms remain future work. | Look for implementations and measured performance on real instances, not only asymptotic bounds. |
A Lean proof is significant evidence about the formal theorem, but it cannot on its own guarantee that the encoded definitions capture every intended informal claim. That is why a public, independent reconstruction matters. The group's open letter invites researchers to inspect, question and explain the result.
ETH False Is Not P = NP
The relationship is one-way: if P = NP, then 3-SAT has a polynomial-time algorithm and ETH is false. But ETH can be false while P is still different from NP. A running time such as 2^(n / sqrt(log n)) is subexponential yet grows much faster than any polynomial. OpenAI's formalized bound has that latter character. The Clay Mathematics Institute still lists P versus NP as unsolved.
Wes's mountain analogy is useful if the shortcut is drawn at the right scale: the claimed path is shorter than the exponential route, but it is not the instant tunnel of a polynomial-time algorithm. For a more technical primer, Scott Aaronson's P versus NP survey explains why this distinction is foundational.
Encryption, Optimization and the "Cheat Code"
The video asks what a future, practical breakthrough might do to cryptography, logistics, drug discovery and AI research. Those are worthwhile questions, but they are not results of this paper. The published ETH claim offers no measured attack on deployed encryption and no general polynomial-time algorithm. Cryptographic systems depend on specific hardness assumptions, parameter sizes and attack models; a worst-case 3-SAT upper bound does not by itself translate into a useful key-recovery procedure.
Even a hypothetical proof of P = NP would not automatically supply a practical algorithm: a polynomial can hide an unusably large degree or constant. The discussion of a universe-level "cheat code" and of simulation-like constants in the video is speculation, not a conclusion from the manuscript. The immediate, defensible implication is narrower: if the proof holds, researchers will need to revisit results that were conditional on ETH and search for sharper algorithmic ideas.
The Other Math and Physics Announcements
OpenAI announced two other research directions alongside ETH. Its local-smoothing manuscript and Lean scope note claim a result with consequences for Kakeya and restriction questions. As with ETH, the public artifacts are material for expert examination, not a reason to skip it.
For physics, OpenAI describes a claimed construction of certain four-dimensional interacting quantum field theories and says an external group is preparing an account. It has not publicly released the same kind of proof package for that claim. It also does not mean the full Yang-Mills existence and mass gap Millennium Prize problem has been solved: Clay still lists that problem as unsolved. Emanuele Viola's 2018 essay arguing that P = NP may be true is an interesting viewpoint Wes cites, not evidence that the open problem is now settled.
What to Watch Next
- Independent reconstruction: follow the ETH group's updates for a plain-language explanation and any corrections.
- Formalization scope: compare any new Lean documentation with the manuscript's strongest theorem.
- Practical algorithms: ask whether anyone turns the proof idea into a solver that beats existing methods on realistic inputs.
- Conditional research: see which ETH-based lower bounds need revised assumptions, rather than assuming all hardness results disappear.
Video Chapters
The claim and the complexity question
| Time | Topic |
|---|---|
| 00:00 | OpenAI's announcement |
| 06:20 | P versus NP |
| 12:35 | The Exponential Time Hypothesis |
| 14:05 | AI and mathematicians |
Consequences and speculation
| Time | Topic |
|---|---|
| 18:10 | The mountain analogy |
| 22:00 | A computing cheat code? |
| 24:30 | Constants and simulations |
| 27:25 | Viola and physics |
Sources and Provenance
- Video and viewpoint: Wes Roth's full discussion and the supplied transcript. Analogies and speculative consequences are attributed to the video.
- Primary research: OpenAI's announcement, math repository, ETH manuscript, Lean scope note, local-smoothing manuscript, and its Lean note.
- Independent context: ETH examination group's letter, Clay P versus NP, Clay Yang-Mills and mass gap, Aaronson's survey, and Viola's essay.
Checked 28 October 2026. This article does not claim independent proof verification, a working solver, or an assessment of unpublished physics materials.