On October 26, 2026, OpenAI published on GitHub a non-peer-reviewed preprint titled "The Exponential Time Hypothesis is False," together with a formal proof written in the Lean theorem prover. The result was generated by an internal OpenAI model, and the company claims it refutes the Exponential Time Hypothesis (ETH), an important conjecture in computational complexity theory. The verification effort is being led by Russell Impagliazzo and Ramamohan Paturi, who proposed the ETH, and by Ryan Williams of the Massachusetts Institute of Technology (MIT). However, the fact that experts are taking part in the verification is not the same as confirmation that the claim is correct.
When a search tries every possible combination, the computation time shoots up as the problem grows. The ETH conjectures that, for a representative logic problem, no amount of algorithmic ingenuity can avoid exponential time. Overturning it would change an assumption that has long served as a yardstick for measuring computational difficulty. At the same time, the explanation that Lean has formally verified the proof alone does not settle whether the result truly refutes the ETH as human researchers understand it.
What the Exponential Time Hypothesis, a "Wall of Computation," Has Claimed
One of the most famous open problems in complexity theory is the P versus NP problem. Roughly speaking, it asks whether P, the class of decision problems solvable in polynomial time, equals NP, the class of problems whose "yes" answers can be verified in polynomial time. The prevailing conjecture is that the two are not equal, that is, . But even knowing that a problem cannot be solved in polynomial time does not determine how much time computation actually requires. To discuss the limits of algorithms in detail, a more probing question is needed: is exponential time unavoidable?
The ETH was proposed in the late 1990s and early 2000s by Impagliazzo, Paturi, Francis Zane and others to address this question. At its center is 3-SAT (the 3-satisfiability problem), a representative NP-complete problem. In 3-SAT, one works with logical formulas built from clauses, each joining at most three literals (variables or their negations) with "or," and then joining the clauses with "and." The problem is to decide whether there exists a truth assignment that makes the whole formula true.
If the number of variables is $n$, there are $2^n$ possible truth assignments. Stated while omitting factors polynomial in the input length, the ETH conjectures that "there exists a constant $\delta > 0$ such that no deterministic algorithm solves 3-SAT in $O(2^{\delta n})$ time." If this is true, 3-SAT also cannot be solved in $2^{o(n)}$ time, that is, subexponential time, where the exponent grows more slowly than $n$. Making an algorithm faster than the brute-force $2^n$ is different from reaching subexponential time. Even if the coefficient in the exponent is reduced to a small positive constant, the running time still grows exponentially.
The ETH is not a proven theorem, but over the past quarter century a great deal of research has assumed it in order to establish lower bounds on computation time. These include graph problems such as maximum independent set and clique, and extend to computational geometry, databases, and computational biology. What these results provide are conditional hardness proofs of the form: "if the ETH is true, this problem cannot be solved faster than a certain complexity." The ETH has served as a standard yardstick for thinking about how far algorithms can be sped up.
The Algorithm and Complexity Claimed in the Preprint
The core of the preprint is the claim that it constructs a deterministic subexponential-time algorithm for "$k$-CNF" formulas, in which the number of literals per clause is bounded by a fixed $k$. The target is not limited to the problem of deciding whether a satisfying assignment exists. The algorithm also handles the counting problem of exactly determining the total number of satisfying assignments, and the memory it uses is said to stay within a polynomial of the input length. For $k=3$, this includes 3-SAT and its counting version, #3-SAT, so if the claim holds it would lead to a refutation of the ETH.
The running time given in the summary of the public repository, expressed roughly while omitting factors polynomial in the input length, takes the following form, where $n$ is the number of variables.
Because the logarithmic term in the denominator grows, once $n$ is sufficiently large this expression becomes smaller than for any fixed positive constant . It therefore satisfies the condition of subexponential time. On the other hand, this expression grows faster than any polynomial of fixed degree $c$, and it does not fall within quasi-polynomial time either. The stated upper bound on running time is still superpolynomial; it does not show that the problem can be solved in polynomial or quasi-polynomial time.
There is, however, a gap between the upper bound claimed in the paper and the one formalized in Lean. In the description of the formalization scope, the exponent, excluding polynomial factors and constants, is given as on the Lean side and in the October 25 version of the paper. Both are subexponential, but the latter gives the smaller bound. This is not merely a notational discrepancy; it should be understood as a difference between the complexity stated in the paper and the complexity that has been formalized.
Moreover, an asymptotic improvement in complexity alone cannot tell us whether the algorithm would beat existing SAT solvers on inputs of realistic size. Actual running time also depends on constant factors and lower-order terms omitted in complexity notation, as well as on implementation. OpenAI itself says that more research will be needed to turn the theoretical progress into practical improvements. The claim and its verification status are summarized below.
| Item | Claim in the preprint | Verification status (as of October 27, 2026) | What this claim alone does not show |
|---|---|---|---|
| Proposition addressed | Refutation of the Exponential Time Hypothesis (ETH) | OpenAI says it was verified in Lean; outside researchers are examining it | A solution to P vs NP, or a proof of $P=NP$ |
| Algorithm | Exactly counts satisfying assignments of fixed-width CNF formulas in subexponential time and polynomial space | Paper and Lean code are public | Practical SAT solvers or faster cryptanalysis |
| Running time | Roughly | The paper and Lean differ in the more detailed upper bounds | Reaching quasi-polynomial or polynomial time |
| Theoretical impact | Premises of hardness assessments that depend on the ETH would change | Stage of independently examining both the correctness of the claim and its consequences | That all NP-hard problems become easy to solve |
Verification with Lean, and What a Formalization Needs to Confirm
According to OpenAI's announcement, the internal model generated the natural-language refutation proof on October 16, 2026, and the company formalized the result in Lean the next day, October 17. Lean is software that checks whether formal statements are correctly derived from definitions, axioms, and lemmas. Steps that human-written papers skip with phrases like "obvious" or "shown similarly" must be filled in formally in a proof to be verified. Still, the fact that code was processed without errors is not necessarily sufficient; one also needs to check whether any unproven parts remain in the lemmas it depends on, and what any additional axioms assume.
With those conditions checked, what Lean guarantees is that the statement written in the code follows under the adopted definitions and axioms. Passing verification does not automatically guarantee that the statement matches the mathematical claim researchers intend. For example, if the definition of a term or the order of conditions differs from the intent, or if an assumption absent from the original problem is added, the proof may be correct yet prove a different statement. In this case, what must be checked includes how inputs are represented, the computational model, and how running time is counted, to see whether the formalized content corresponds to a refutation of the real ETH.
Scrutinizing this correspondence and the argument itself, and organizing it into a form the research community can understand, is the role of Impagliazzo, Paturi, Williams and others. In an open letter, the three state explicitly: "Our involvement should not be taken as a guarantee that this claim is correct." Their aim is an understanding that lets other researchers reconstruct the argument, raise questions, and build further research on it. Beyond machine verification, work is needed to clarify what the proof means and what consequences it carries.
As for the status of the published materials, OpenAI describes them as "raw research data" rather than a finished academic paper. The company says it does not seek academic credit for discoveries by its internal model and leaves judgments about credit and priority to the research community. For now, the publication of materials on GitHub should not be treated as settling the conclusion; progress in independent expert scrutiny needs to be watched.
What Would Change If the Claim Holds
Even if the proof is correct and the refutation of the ETH holds, it would not by itself resolve the P versus NP problem. This is because the complexity result does not show that 3-SAT can be solved in polynomial time. As for RSA and elliptic-curve cryptography, their security does not rest on the ETH itself; the practical attack capabilities against problems such as integer factorization and discrete logarithms need to be assessed separately. From the subexponential-time claim alone, one cannot say that practical cryptographic keys could be broken.
On the theoretical side, research that has estimated lower bounds on computation time based on the ETH would need to be reexamined. For example, for problems that were said to be unsolvable in $2^{o(n)}$ time if the ETH is true, the grounds for treating that lower bound as a real limit of computation would be lost. However, the conditional theorems themselves, "if the ETH is true, the lower bound holds," would not become false. Whether genuinely faster algorithms can be obtained for each problem, and how large the improvement would be, must be examined case by case. The three researchers' letter likewise points out that the interpretation of research may change, while noting that the accumulated ideas, reductions between problems, and techniques retain their value.
On the other hand, scrutiny might uncover flaws in the argument or the formalization, leading to the judgment that the claim does not hold. Beyond the correctness of the algorithm, the complexity estimate and the correspondence between the formalized statement and the original problem must also be checked. Even if part of the proof is correct, one cannot conclude that the ETH has been refuted until every step needed for the conclusion has been verified. Conversely, if this proof fails, that would not prove the ETH to be true.
Unreviewed Claims and Evaluating Proofs in the AI Era
This is not the first time a preprint claiming to refute the ETH has been published. In 2021, a paper titled "The #ETH is False, #k-SAT is in Sub-Exponential Time", which claimed to refute the counting version of the ETH, was submitted to arXiv. Having such a claim posted in a public repository is distinct from having its correctness confirmed by the research community. What is distinctive here is that, in addition to an argument generated by an AI model, a Lean formal proof that can be checked mechanically has also been released.
This case raises not only the question of AI's ability to tackle open problems but also how research credit should be evaluated. Suppose an AI outputs a candidate proof: how should we regard the work of researchers who read and interpret it, correct errors, simplify the argument, and explain its mathematical meaning? In their open letter, Impagliazzo and colleagues expressed concern that recognition may skew toward whoever announces first or holds powerful tools, leaving verification, exposition, and follow-on research undervalued. They also describe the question of early access to results, and support for students and researchers facing changes in research methods, as issues the whole community should discuss.
OpenAI says it did not require outside researchers to sign nondisclosure agreements (NDAs), and that participation was voluntary and unpaid. Researchers work from an independent standpoint and are free to discuss and publish interim findings and conclusions. At the research group's request, the company also agreed to release raw data for independent verification and to fund a conference to discuss the impact of this result on the field as a whole. This effort is thus one attempt at how to support publication, verification, and understanding of results.
What has been made public so far is a paper claiming to refute the ETH and a formal proof for examining that claim. The key questions going forward are whether the formalized definitions and complexity estimates correspond to the real ETH, and whether independent researchers can confirm and explain the argument. Whether it can be concluded that the ETH has been overturned will be decided after that scrutiny.