Deep Dive — Exponential time hypothesis is false, solvers unaffected

Russell Impagliazzo, who proposed the Exponential Time Hypothesis with Ramamohan Paturi in 1999, told the New York Times on 6 November that watching OpenAI's models refute it was "very shocking news," adding that most researchers had expected stricter versions of the assumption to fall first, the Times reported.

Five days earlier, on 31 October, two researchers posted a note to arXiv that did the arithmetic nobody in the coverage had done: they went into OpenAI's appendix, pulled out the constants the preprint leaves hidden inside its big-O notation, and asked at what size a formula would have to be before the new algorithm actually beats trying every assignment. The answer is a formula with more than a billion binary digits. Fabio Dias and Yvens Lima put it plainly in their note: the proof certifies no speed-up over brute force "for any input of bounded density that could ever be written down."

Both statements are true at once, and the distance between them is the most interesting thing in AI research this month. The theorem is a real result about the limits of computation. The algorithm is a claim about what happens as inputs grow toward infinity, and it says nothing useful about any input a machine can hold.

The assumption that priced a field

ETH says that solving 3-SAT — deciding whether a Boolean formula built from three-variable clauses can be satisfied — cannot be done in time 2^δn for any fixed δ above zero. In plain terms: no shortcut beats exponential growth in the worst case. It is a stronger claim than P ≠ NP, and a far more useful one, because it is quantitative. Hundreds of papers in graph theory, computational biology, databases and computational geometry derive "you cannot do better than this" results by assuming it holds. Fine-grained complexity is largely built on it.

That is why the constant matters more than the exponent. A bound written as 2^(C·n·g(n)), where g(n) shrinks toward zero, beats brute force's 2^n only when C·g(n) drops below 1. The crossover point is a function of C, and C is exactly what a paper hides when it writes O(·). With a hidden constant of 2 the general bound wins only past about 10^32 switches; at 3, past 10^126; at 10, past 10^3517. The observable universe holds roughly 10^80 atoms, so the middle case is already beyond anything physical.

What the models produced

OpenAI published the claim on 26 October as one of three results, alongside a solution to the local smoothing conjecture and a claimed existence proof for quantum chromodynamics in four dimensions — the release we went through on the day in Exponential Time Hypothesis is false, OpenAI and Anthropic say. The manuscript, dated 25 October and running 67 pages, is titled "The Exponential Time Hypothesis is False." The company says its model found the argument on 16 October and that it was formalized in Lean a day later, and it released both the writeup and the formalization as public artifacts rather than as a paper, describing them as "a form of raw research data," according to OpenAI's announcement — the same ship-the-artifacts pattern it used for 722 math manuscripts from a model nobody can run.

The algorithm is deterministic, uses polynomial space, and does more than decide satisfiability — it counts the satisfying assignments exactly. Its running time is 2 raised to n·log log n/√log n, which is subexponential because that exponent divided by n tends to zero, just very slowly: roughly the square root of the number of digits in n. At bounded clause density the bound improves to n/√log n.

The mechanism is worth understanding, because it explains both why the result works and why it cannot be pushed into a solver. Picture a dial T that rewires which switches each rule reads. A clause that used to test switch 2 now tests a blend: (1−T) times switch 2 plus T times switch 3. At T=0 you have the original formula. At certain other dial positions the rules no longer connect the variables into one tangled net — they split into independent teams, which may only exchange a few coarse summaries, such as how many switches in a team are on. Count each team separately, multiply, and you have computed the count at that dial position.

The number the counting recipe returns is a polynomial in T, and a polynomial is rigid: a few readings, plus derivatives at those readings, pin it down everywhere. So compute it at the positions where the formula splits, reconstruct the curve, and read off its value at T=0. The three costs — counting inside a team, enumerating summary combinations, and taking ever higher derivatives — pull against each other, and the technical heart of the preprint is a construction that holds all three below 2^n while the teams shrink to a vanishing fraction of the variables.

Two details matter for what follows. First, the Lean formalization proves a slightly weaker exponent than the manuscript's headline: n(log log n)²/√log n, which is still subexponential, so the ETH claim survives the downgrade. Second, Anthropic released a 49-page companion paper making the same claim within hours, and its own text says that on formulas with five clauses per variable the method would not beat brute force below 10^10,000 variables — a number with no physical referent at all.

A billion binary digits

Dias and Lima's contribution is not to dispute the proof. They take it at face value and say so; the note is an arXiv preprint, not peer-reviewed, and its purpose is narrower than refereeing. They do three things: explain the interpolation algorithm in plain terms, tabulate where the bounds bite as a function of the hidden constant, and then trace the constants through the preprint's own tensor-contraction appendix.

That last step is the one that lands. For every input of bounded density, the running time the appendix certifies stays above the brute-force 2^n unless log base 2 of (n + m) — the number of switches plus rules — exceeds 1.03 billion. For random 3-CNF at the satisfiability threshold, the bar is log base 2 of n above 5 × 10^11. Those are not large numbers in the way 10^126 is large; they are large in a way that matters, because a formula with a billion binary digits cannot be stored, let alone read, by any computer that will ever exist. The bound is subexponential in the limit and provides no guarantee whatsoever at any size below the limit.

The note also runs experiments, and they are a useful reality check. On the SATLIB random 3-SAT families, the rigorous lower bound on treewidth grows linearly with n while the heuristic bounds grow slowly, and at the sizes tested — 20 to 250 variables — the preprint's own algorithm would fall back to direct summation. None of this is evidence against the theorem. It is evidence that the theorem was never about those instances.

The method has a floor

The second half of the note is more interesting to theorists than the first. The clause-product form of the algorithm has a structural limit, and it comes from a one-line algebraic fact: each occurrence of a variable carries a coefficient that equals 1 at T=0 and can vanish at only a few dial positions, so at any single position only a few links can be cut. A tangled formula cannot split there, and that position is expensive.

The consequence is a set of barriers in a cost model that charges what the preprint's own evaluation pays. Polynomial cost would force the formula's treewidth down to O(log²n). On random 3-CNF above clause density 3 the scheme costs at least 2^Ω(√n), and with the preprint's method of combining teams, at least 2^Ω(n^(1/3)) even on a simple chain of rules.

Scope matters here, and the authors are careful about it. These are limits on one route — the clause-product scheme — not on the result. The parity-check form and the tensor contraction escape them, because they break the link between variable occurrences and the degree of exact recovery. Whether similar barriers hold for those routes is open, and the gap between 2^Ω(√n) and the claimed 2^(O(ρ(n))) on expanding inputs is explicitly left unresolved. This is a barrier for a method, in the same spirit as the known limits of the laser method for matrix multiplication — not a claim that ETH is secretly true after all.

Who checked it, and what wrote the check

The review is being run by the people who invented the assumption. Impagliazzo and Paturi at UC San Diego, with MIT's Ryan Williams, agreed to shepherd the result without pay and without nondisclosure agreements, asked OpenAI to publish every artifact, and asked it to fund a conference on what the result means. Their joint statement is careful: "Our involvement should not be taken as certification of the claim."

Williams, who once called an earlier OpenAI proof dump a "DDOS attack on mathematicians," told TechCrunch that parts of the argument are routine but "there are two or three alien-looking parts, and it's exactly these parts that I saw made me think, wow, this is something that the whole community needs to work on together," he said. Others were more blunt about the surprise. "This came as a complete surprise, a shock. Nobody I know expected it," Fedor Fomin of the University of Bergen told New Scientist, while Stefan Szeider of TU Wien said he expects the result to withstand scrutiny — with the caveat that someone still has to confirm the formally proven statement means what its authors say it means, per New Scientist.

The provenance of the check is its own story. Dias and Lima disclose in the note's methodology section that the analysis was carried out with Claude Opus 5.5 through Claude Code — reading the preprint, deriving the arguments, extracting the constants from the appendix, writing and running the verification code, and drafting the text. A second instance of the model, with no access to the authors' working notes, refereed the draft against the preprint, and its report is why the limits were narrowed to the clause-product route. The authors directed the work and take responsibility for the claims. So the most careful audit of an AI-generated proof so far was itself largely written by a different company's AI, refereed by a third pass of the same system.

That is not a scandal. It is the only way the check could have arrived in five days. It is also the reason to read the note's scope qualifications closely rather than the headline. Who gets credit for a result whose author is a model, whose referee is a rival lab's model, and whose reviewers invented the claim in the first place is the question we worked through when math's credit system turned out to be built for humans, and nothing about this release resolves it.

What actually changes

As a statement about computation, the refutation is large. Hundreds of conditional lower bounds lose their premise. They are not wrong; they are no longer proven, which for a field that publishes "you cannot do better than this" as its main product is a substantive loss. OpenAI's paper says the result also refutes SETH, Gap-ETH and NSETH. P versus NP is untouched, because a subexponential bound is not a polynomial one, and OpenAI's own writeup says turning theoretical advances into practical improvements "will require significant further research."

Nothing about encryption changes this month. Williams's first question to OpenAI's science lead Dan Roberts was whether any cryptographic system had become insecure; the answer, as the numbers above suggest, is no. Ed Felten of Princeton called the Times framing "deeply misleading" on Bluesky, arguing the result has theoretical importance and little immediate practical consequence — a fair reading of a story that put chip design and broken encryption in the headline of a paper whose own appendix rules both out at any feasible size.

What does change is the shape of the claim. A frontier lab can now publish a true, machine-checked theorem whose practical content is nil, and the field has no ready vocabulary for that. The old categories were "correct" and "incorrect"; the new one is "correct, and priced at a size no machine can hold." The verification apparatus worked exactly as designed — Lean checked the proof, named humans checked the meaning, a competitor checked the release — and the output is still a result that will be cited for a decade and used by nobody.

What to watch

The fixable part is the constants. OpenAI published no C, which is what made the note necessary; a lab that wants its results understood rather than merely admired should state the crossover size alongside the asymptotic bound. Watch whether the revision does.

The substantive question is whether the parity form and the tensor contraction survive the same kind of audit. If they do, the subexponential bound stands and the barrier is a curiosity about one route. If they do not, the field is back where it started, with a Lean-verified proof of a statement whose algorithm has a floor.

Then there is the honest test of practical value, which is whether anyone turns 2^o(n) into a faster count at 200 variables. Williams told followers that serious practical progress is plausible within 12 months, "or we may see nothing of the sort." The interim notes from the review group, and the conference OpenAI agreed to fund, are where that gets settled.

Until then the accurate sentence is the awkward one. The Exponential Time Hypothesis is false, and every SAT solver in production behaves exactly as if it were true.