On 26 October 2026, OpenAI made public a manuscript called The Exponential Time Hypothesis is False. Its author line says only “OpenAI”. According to OpenAI's own repository, it was produced by an unnamed, unreleased internal model, and a version of its main theorem has been checked by Lean, a program that verifies mathematical proofs step by step. It came out alongside two other claimed results, in mathematics and physics, which this piece leaves aside.
The unusual part is who is checking it. The hypothesis in the title was proposed in 1999 by Russell Impagliazzo and Ramamohan Paturi. The two of them, together with Ryan Williams, now lead an independent working group that will examine the proof. The materials were released immediately at the group's request, and the group has reportedly said that taking part is not an endorsement. Until that review is done, this is a claim, and the rest of this page treats it as one.
To make sense of it, we'll take four questions in order:
What is the puzzle at the centre of all this?
What exactly is the Exponential Time Hypothesis, or ETH?
Why did anyone care whether it was true?
What would follow if OpenAI is right, and how sure can we be?
Chapter 2 / 9
The puzzle: three switches, four rules
Let's start with something you can solve in your head. There are three switches, x, y and z, and each one is either T (true) or F (false). There are four rules. A rule is satisfied when at least one of its parts holds. Your goal is a setting of the switches that satisfies all four rules at once.
More ·How to read NOT and OR
“x OR y OR z” is satisfied when at least one of x, y, z is T. “NOT x” holds when x is F. So “NOT x OR y” is satisfied unless x is T and y is F at the same time.
Tap a switch to flip it
Rule 1x OR y OR zon
Rule 2NOT x OR yoff
Rule 3NOT y OR zon
Rule 4NOT z OR NOT xon
Predict
There are 2 × 2 × 2 = 8 ways to set the three switches. How many of them light all four rules?
Answer the question above to unlock
x
y
z
Result
What you just solved is a satisfiability puzzle. You have some yes/no switches and a list of rules, each saying at least one of these must hold, and the question is whether some setting satisfies every rule at once. When each rule mentions at most three switches, computer scientists call the puzzle 3-SAT: SAT for satisfiability, 3 for at most three switches per rule. In their vocabulary the switches are variables, the rules are clauses, and a setting that works is a satisfying assignment.
The only sure-fire method we have met is the one the table used: try every setting. With n switches there are settings, so brute force takes on the order of steps. Three switches give 8 rows; thirty give about a billion.
One puzzle stands for a whole family
Notice something about what you just did. Checking a setting took a glance: go down the rules one by one. Finding a setting meant trying them. Many famous problems have that same shape: an answer is quick to check, but finding one seems to need a search. Colour the dots of a network so that no two linked dots match. Plan a route that visits every city exactly once. Computer scientists call the problems where a proposed answer is quick to check NP. Being in NP doesn't make a problem hard, since easy problems are in it too, but for its hardest members, finding an answer seems to need a search.
Those hardest members, the NP-complete problems, are tied together tightly: they can all be rewritten as one another. A 3-SAT formula can be turned into a colouring problem with the same answer, and a colouring problem into a 3-SAT formula. And for the four problems below, the rewrite from 3-SAT stays about the same size: a formula becomes a graph with about as many dots as it has switches and rules. The rewrites back into 3-SAT aren't guaranteed to stay that small.
Quick to check · seems to need a search to find
Graph colouring
Give each dot one of 3 colours so that no two linked dots match.
check: look at each link · find: try colourings
Hamiltonian cycle
A route through every city exactly once, ending where it started.
check: walk the route · find: try routes
3-SAT
the switches puzzle
check: read each rule · find: try settings
3-SAT rewrites into each, about the same size
Vertex cover
Pick a few dots that touch every link.
check: look at each link · find: try sets of dots
Clique
Find k dots that are all linked to each other.
check: look at each pair · find: try groups
All five problems are NP-complete. “Size” counts switches and rules for 3-SAT, and dots for the others.
That is why a puzzle about switches matters. The paper itself calls k-SAT “the canonical NP-complete problem”: the standard stand-in for the whole family. Because the members rewrite into one another, a genuinely fast way to solve 3-SAT, one whose work grows like a fixed power of n instead of doubling with every switch, would hand you fast ways to solve all of them. And a fast way to solve any one of them would hand you one for 3-SAT.
Chapter 3 / 9
The doubling wall
Brute force is fine for three switches. Scroll on and watch what each step up in n does to the table. There is no log scale here: each new bar fills the panel, and the one before it is redrawn at its true size beside it.
Chapter 4 / 9
The bet: “you can't get under the wall”
Clever algorithms have lowered the multiplier per switch, from ×2 for brute force to about ×1.307. But every one found so far still pays some fixed multiplier for each extra switch. Is that a law, or have we just not been clever enough?
In 1999, Russell Impagliazzo and Ramamohan Paturi made a precise bet, the Exponential Time Hypothesis (ETH). It says that every algorithm for 3-SAT, however clever, pays on average at least some fixed multiplier for each extra switch, on the hardest puzzles of each size. That multiplier might be tiny, ×1.001, but it never fades to ×1.
Notice the word hypothesis. Nobody has proved ETH. It is an unproven assumption, a foundation stone that researchers chose to build on.
You have probably heard of a famous cousin, P ≠ NP. Both are bets about the same unknown, because nobody knows the fastest possible algorithm for 3-SAT. Where could it sit? The figure shows four possible answers, sorted by how quickly the work grows as you add switches. Two are algorithms we have, and two are speeds nobody has found.
More ·The formal statement
ETH: there is some constant such that every algorithm that correctly solves 3-SAT needs at least steps on some formulas with n variables. Since , that is an average multiplier of at least per variable on the hardest formulas. Equivalently, there is no algorithm for 3-SAT, where means something that grows more slowly than any fixed fraction of n. Running times of the form are the subexponential ones: their average multiplier per variable fades toward ×1.
Apply
Suppose someone proved that 3-SAT can be solved in about steps. Which assumption would be broken?
Chapter 5 / 9
What was built on the bet
A link, not a proof
Researchers usually can't prove outright that a problem has no fast algorithm. (If they could do that for 3-SAT, P vs NP would be settled.) What they can prove is a link.
Remember the family from chapter 2, and graph colouring in it? 3-SAT can be rewritten as colouring at about the same size. That lets a result read:
Graph colouring has no algorithm on graphs with n vertices, unless ETH fails.
The proof is the rewrite from the family figure. It turns any 3-SAT formula into a colouring problem with about as many dots as the formula has switches and rules. So a much faster colouring algorithm, one whose multiplier per dot fades toward ×1, would also be a much faster 3-SAT algorithm, and that would break ETH. As long as ETH holds, colouring is stuck paying a fixed multiplier per dot too. The same move, with other rewrites, gives lower bounds for Hamiltonian cycle, vertex cover, clique and many more problems.
Explain · think, then reveal
A paper proves “graph colouring has no algorithm, unless ETH fails.” In your own words: what did it actually prove, and what would make the statement stop telling us anything about hardness?
A bolder bet: SETH
ETH only says that 3-SAT's multiplier never fades to ×1. There is a much bolder bet, the Strong Exponential Time Hypothesis (SETH). Let the rules get wider, with 4, 5 or 10 switches each, and SETH says the best possible multiplier climbs toward ×2, getting as close to it as you like. For wide rules, brute force is essentially unbeatable.
Multiplier per extra switch, for the best possible algorithm
The dots are what the best algorithms so far achieve (the PPSZ algorithm), not proof of what is possible, so they are not evidence for SETH. SETH bets that the true floor climbs to ×2. Beyond 6 switches per rule, the arrow is schematic.
Bolder bets buy stronger results. The most famous one built on SETH: Backurs and Indyk proved that edit distance, the measure of how different two strings are and a close relative of what diff computes, can't be computed in much less than quadratic time, unless SETH fails. Hold on to SETH and edit distance. They come back in chapter 7.
More ·Why does SETH imply ETH?
ETH only says 3-SAT needs some exponential with , and could be close to 1. SETH says that for wide enough clauses the base gets arbitrarily close to 2. If SETH is true, wide-clause SAT needs exponential time, and that in turn forces 3-SAT to need exponential time, which is ETH. So SETH implies ETH.
Compare
ETH and SETH are both unproven bets. Which one is riskier, that is, easier to turn out wrong?
What rests on ETH and SETH
Graph colouring, Hamiltonian cycle, vertex cover: no algorithm
unless ETH fails
k-Clique: no algorithm, so brute-force search is essentially optimal
unless ETH fails
Edit distance (a close relative of diff): no algorithm
unless SETH fails
… and many more
SETHbolder · SETH ⇒ ETH
ETHthe Exponential Time Hypothesis
Arrows point from each theorem to the assumption it rests on. SETH sits on top of ETH because SETH implies ETH.
Chapter 6 / 9
The claim
Now OpenAI's claim, stated precisely. Three symbols first. n is the number of variables and m the number of clauses. is the logarithm of n, which grows very slowly: going from a thousand variables to a million only doubles it. And is a small term that shrinks toward zero as n grows.
The manuscript claims a deterministic algorithm (no coin flips) that counts the satisfying assignments of any SAT formula whose clauses have a fixed width k, 3-SAT included, using only a polynomial amount of memory. Its running time is
The first factor is an ordinary polynomial, which barely matters next to the second. In plain terms the cost is roughly .
Counting is at least as hard as deciding: if the count is above zero, the formula is satisfiable. And grows more slowly than any fixed fraction of n, so the 3-SAT case is a algorithm for 3-SAT. In per-switch terms, its multiplier fades toward ×1 as n grows: very slowly, but it does fade. That is exactly what ETH bet could never happen. The repository's summary puts it in one line: “The case of 3-SAT refutes the Exponential Time Hypothesis.”
More ·What the paper actually proves
The theorem covers every fixed clause width : a deterministic algorithm counts the satisfying assignments of a k-CNF formula (a k-SAT formula) with n variables and m clauses in the time above, in polynomial space. The main theorem gives in general, improving to when the number of clauses is at most a constant times n. The paper states that this refutes ETH, SETH, and two related hypotheses, Gap-ETH and NSETH.
Where does that land on the ladder?
Predict
The claimed algorithm is subexponential, and the old best was exponential. When do you expect it to beat the old best () on real formulas?
The growth chart appears once you've answered.
Chapter 7 / 9
If it holds: what falls, what stands
Back to the foundation. Suppose review confirms the claim. What happens to everything that rested on ETH and SETH?
Predict
The famous result that edit distance (a close relative of what diff computes) can't be done much faster than quadratic time assumes SETH, not ETH. If OpenAI's claim holds, what happens to that result?
The foundation, before the claim
Graph colouring: no algorithm
unless ETH failsclaimed disprovedThe paper also claims a colouring algorithm of its own.
Hamiltonian cycle, vertex cover: no algorithm
unless ETH failsunproven again — not disproved
k-Clique: no algorithm, so brute-force search is essentially optimal
unless ETH failsunproven again — not disproved
Edit distance (a close relative of diff): no algorithm
unless SETH failsand unless OVC failsSETH basis lost · still stands on OVC
… and many more
Longest common subsequence, regex matching: lower bounds
unless OVC failsstill stands
SETHbolder · SETH ⇒ ETHrefuted (claimed)
ETHthe Exponential Time Hypothesisrefuted (claimed)
OVCOrthogonal Vectors Conjecture (not refuted)
A theorem of the form “no fast algorithm, unless ETH fails” stays true when ETH fails. It just stops telling us anything about hardness.
The diagram updates once you've answered.
Three tempting conclusions
“So P = NP?”
No. The claimed running time, roughly , is still far above any polynomial, and ETH failing says nothing either way about P vs NP. The paper itself notes that its result doesn't imply subexponential algorithms for general NP problems, because the usual translations between problems can blow up the input size.
“So crypto is broken?”
No. RSA and AES never rested on ETH. And “subexponential” can still mean astronomically slow: factoring, the problem behind RSA, has had a subexponential algorithm, the general number field sieve (GNFS), for decades, and properly sized RSA keys are still secure.
“So Hamiltonian cycle and the rest are fast now?”
No. Losing the proof that a problem is hard is not the same as finding a fast algorithm for it. A bound whose condition fails is unproven, not reversed. Any faster algorithm for a particular problem still has to be found and proved on its own.
Chapter 8 / 9
Is it true? What “verified” does and doesn't mean
“Verified in Lean” is strong evidence. It is also narrower than it sounds. Lean is a proof assistant: you state a theorem in its formal language, supply a proof, and its small trusted core, the kernel, checks every step. OpenAI's repository includes the formal statement as a challenge file and invites anyone to re-run the check with a tool called Comparator. Here is what that check does and doesn't settle.
Lean's checker guarantees
Humans still have to confirm
StatementThe proof proves exactly the stated formal theorem.
StatementThe formal definitions mean what the paper says: the model of a computer (a Turing-machine model defined in the challenge file), how a formula is encoded, what counts as a step.
StrengthIt uses only the three standard axioms the check permits.
StrengthThe paper's sharper headline bound holds. The bound that was formalised is slightly weaker (though still enough to refute ETH).
ScopeLean's kernel accepts every step of the formal proof.
ScopeThe informal parts of the manuscript are right. The repository's own README warns that some unformalised results could have issues.
More ·The exact formal bound
The Lean theorem proves a running time of times a polynomial, with polynomial memory, for the machine model defined in the challenge file. That's slightly weaker than the paper's headline bound, but it still grows more slowly than any , so it is still enough to refute ETH.
The gap in the right-hand column isn't hypothetical. When OpenAI announced an earlier Lean-verified result, on the Navier–Stokes equations, readers raised the concern that Lean had verified a weaker assertion than the headline (as reported by Gizmodo). No such problem has been reported for the ETH formalisation.
How the claim surfaced
16 OctModel produces the claimed disproof (as reported)
17 OctFormalised in Lean (as reported)
25 OctDate on the manuscript
26 OctMade public; review group announced
The first two dates come from press accounts of OpenAI's announcement (Unite.AI, The Next Web), not from the repository.
Explain · think, then reveal
Lean's checker accepted the proof. Name one way the result could still turn out to be wrong, or weaker than advertised.
What to watch for
The working group's write-up of the proof.
Whether experts judge the Lean definitions, the machine model and the formula encoding, to be faithful.
Independent re-checks and re-implementations of the argument.
Whether the paper's sharper bound, the one that wasn't formalised, holds up.
One more piece of context, about the source rather than this result: on 7 October 2026 the same repository withdrew three unrelated manuscripts after a sign error was found. That says nothing about the ETH proof. It is a reminder that these manuscripts are, in the README's words, “best understood as a form of raw research data”.
Chapter 9 / 9
The whole story in five statements
Sort · one statement at a time
Suppose the claim survives review. For each statement, does it follow?
b3-SAT can be solved in time.
cRSA encryption is broken.
dMost hardness results proved “unless ETH fails” become unproven, not false.
Recap
3-SAT is the switches puzzle, and it stands for a whole family of problems that rewrite into one another. Brute force doubles its work with each switch.
ETH bet that every 3-SAT algorithm pays a fixed multiplier per extra switch; SETH bet that for wide rules that multiplier is ×2. Both were always assumptions, never theorems.
Many hardness results were built on those bets: colouring and its relatives on ETH, edit distance on SETH.
OpenAI claims an algorithm just under the wall. If review confirms it, most ETH-based results become unproven again (for colouring, the paper also claims a fast algorithm outright) and SETH falls too, though some bounds, edit distance's among them, still stand on a weaker assumption (OVC). P vs NP and today's cryptography are untouched.