October 27, 2026 — The claimed result has a released Lean formalization; independent confirmation remains pending.
If a problem has a trillion possible answers, surely a computer has to try a trillion possibilities?
That sounds like common sense. Make the problem bigger, multiply the possibilities, and eventually even the fastest machine runs out of time. We hear versions of this story about scheduling aircraft, designing chips, and finding the best combination of almost anything.
Now OpenAI says one of its internal AI models has overturned a major conjecture about how quickly certain problems can be solved. Its October 26 announcement reports a disproof of the Exponential Time Hypothesis, or ETH, checked in the Lean proof assistant. Independent researchers still need to examine it.
To understand why that could matter—and why your laptop is not suddenly about to solve every difficult problem—we need to look inside that trillion-possibility story.
Imagine organizing a trip. Alice, Ben, and Cara each have a yes-or-no decision: come along or stay home. There are three rules:
- At least one of Alice or Ben must come.
- If Alice comes, Cara must come too.
- Ben and Cara cannot both come.
Can you make everyone’s conditions work?
Yes: invite Alice and Cara, and leave Ben at home.
You have just solved a tiny instance of SAT, short for Boolean satisfiability. “Boolean” means that each variable has two possible values, true or false. “Satisfiability” asks whether some assignment of those values makes all the conditions true. The formal version uses AND, OR, and NOT to express the rules. A SAT solver finds a working assignment or establishes that none exists.
Three people give eight possible guest lists. Thirty give more than a billion. A hundred give about 1.27 million trillion trillion combinations.
Yet a little reasoning can eliminate many possibilities at once. If Cara cannot come, Alice cannot come either. You do not have to test every guest list containing Alice to discover that each one fails. SAT algorithms exploit logical consequences like this, sometimes with extraordinary success.
The difficult question is how far that reasoning can take us on the hardest instances.
A particularly important version is 3-SAT. Here, each rule is a small OR statement containing at most three variables or their negations: “Alice comes OR Ben stays home OR Cara comes.” The whole collection of rules must hold simultaneously.
The “3” describes the maximum number of statements in each rule, not the total number of decisions. A 3-SAT problem can contain millions of variables and clauses.
This apparently modest format is remarkably expressive. SAT and 3-SAT are NP-complete: other decision problems with short, efficiently checkable evidence for a “yes” answer can be translated into them with only a polynomial increase in size. That connection, explained in Stephen Cook’s account of P versus NP, makes SAT a central meeting point for questions about computational difficulty.
But being NP-complete does not prove that a problem requires exponential time. That stronger claim is where ETH enters.
In their foundational work, Russell Impagliazzo and Ramamohan Paturi investigated how the difficulty of SAT changes with clause size. ETH asserts that 3-SAT has an unavoidable positive exponential rate in the worst case.
Brute force takes roughly 
A running time such as 
ETH concerns a guarantee across all inputs. Solving a large collection of useful examples quickly would not refute it; an algorithm must handle the difficult cases too.
Why did researchers take this conjecture so seriously? Partly because different lines of research kept pointing toward the same limit. In his 2014 essay “The Scientific Case for P≠NP”, Scott Aaronson described how algorithms and reductions developed independently repeatedly fitted together without producing a subexponential SAT algorithm. The apparent coordination helped make an exponential barrier seem like an explanation rather than a guess.
It was persuasive evidence. It was never a proof.
OpenAI’s new manuscript, The Exponential Time Hypothesis is False, claims an algorithm that crosses precisely this boundary.
According to the release record, the algorithm does more than decide whether a valid assignment exists: it counts exactly how many assignments work. If the count is zero, the answer is no; otherwise, it is yes. The claimed algorithm is deterministic, uses polynomial space, and runs in subexponential time for every fixed clause-size limit.
For the guest-list example, that is the difference between establishing that some invitation list works and calculating how many lists work—without individually enumerating all of them.
OpenAI says its model found the argument on October 16 and that the result was formalized in Lean the following day. Its announcement states:
“Surprisingly, our system has recently proved that the ETH is false, a result that was subsequently verified in Lean.”
That is a substantial claim. The public status remains a claimed breakthrough with formal verification reported by its producer, awaiting independent examination.
The running-time improvement also needs careful description. Roughly speaking, the exponent involves 
There is a further distinction in OpenAI’s formalization scope note: the Lean theorem establishes a slightly weaker time bound than the manuscript’s sharper general bound. Both remain subexponential. The formalization therefore addresses the central ETH claim, while the strongest quantitative statement in the manuscript should be distinguished from the checked bound.
This raises an understandable question: if Lean has checked the proof, what remains for people to check?
Lean is a proof assistant. As its official introduction explains, formal verification requires mathematical claims to be supported by detailed proofs grounded in definitions, axioms, and rules of inference. It offers far stronger evidence than an AI generating pages of plausible mathematical prose.
But the formal statement must express the intended claim. Researchers still need to scrutinize how the computation is modeled, how inputs are encoded, how resources are counted, and whether the resulting theorem corresponds to ETH as used in the literature. They can also independently reproduce the verification and work toward an explanation that other researchers can understand and use.
Checking a proof and understanding its significance are related jobs. Neither makes the other unnecessary.
The examination is being organized by Impagliazzo, Paturi, and MIT’s Ryan Williams. As The Next Web reports, quoting their open letter:
“Our involvement should not be taken as certification of the claim.”
That sentence deserves to travel with the headline.
If the result holds, its first consequences would be mathematical. The ETH lower-bound literature connects the hypothesis to problems involving graphs, geometry, constraints, and more. A typical argument shows that a sufficiently fast algorithm for some other problem would produce a SAT algorithm fast enough to violate ETH.
Such an argument establishes a conditional limit. Remove the hypothesis, and that justification for the limit disappears.
The papers do not thereby become worthless. Their reductions and unconditional results can remain correct. Some lower bounds may survive under other assumptions. What changes is which running-time barriers researchers can still defend—and which possibilities deserve renewed investigation.
For example, Dániel Marx’s work on constraint satisfaction and database queries combines algorithms for certain structures with ETH-dependent arguments that wider classes cannot be handled as efficiently. A refutation would undermine that negative justification while preserving the positive algorithms. This is the kind of careful separation required across the literature.
The stronger hypothesis, SETH, would also fall. It says, roughly, that no fixed improvement in the exponential base below 2 works across every fixed clause size. Because SETH implies ETH, a valid ETH refutation defeats both assumptions.
For everyday computing, however, the consequences are less immediate.
An asymptotic theorem describes what eventually happens as input sizes grow. It does not establish that the proposed algorithm beats existing software at useful sizes. Hidden constants, the cost of intermediate computations, and memory requirements can overwhelm an attractive asymptotic bound. In this case, even the exponent’s improvement develops very slowly.
The practical opportunity would be to understand the ideas well enough to simplify them, strengthen the guarantees, or extract components that help real solvers. Better tools for checking hardware designs, handling constraints, or planning complicated systems are plausible research goals. They are not demonstrated outcomes of the announcement.
Nor would the result settle P versus NP. Polynomial time—growth such as 
In his response to the announcement, Aaronson emphasizes another limitation: the result concerns SAT with a fixed clause-size bound. It does not automatically provide the same improvement for unrestricted formula or circuit satisfiability. Translating between problems can enlarge an instance enough to consume the advantage. “NP-complete” does not mean that every improvement transfers with its exact running time intact.
A trillion possible answers are not necessarily a trillion required operations. Rules create structure. An algorithm can use that structure to eliminate possibilities in groups, reuse work, or reach a conclusion without inspecting every candidate separately. We already knew that much.
ETH made a deeper wager: however successfully we exploited that structure, the worst cases of 3-SAT would retain a positive exponential rate. OpenAI now claims that wager was wrong.
If independent scrutiny confirms the result, computers will not wake up with infinitely more power. Researchers will have learned that an influential limit on their power was drawn in the wrong place.
The next question will be how much useful computation lies beyond it.