OpenAI vs. the Exponential Time Hypothesis: What's Verified

OpenAI published a preprint this week titled "The Exponential Time Hypothesis Is False."[^1] The Exponential Time Hypothesis, or ETH, is a conjecture that complexity theorists have leaned on for about a quarter of a century. The people now checking the proof are the ones who proposed it, and their first public statement was a disclaimer: their involvement "should not be taken as a guarantee that this claim is correct."[^2]

That is the right tone for a story with three headline claims, three different levels of evidence, and one very large gap between "a proof exists" and "the proof is right."

What the Exponential Time Hypothesis Actually Says

3-SAT asks whether a Boolean formula, written as clauses of three literals each, can be satisfied by some assignment of true and false to its variables. It is the canonical NP-complete problem. The best known algorithms still take time exponential in the number of variables, n.

ETH, proposed by Russell Impagliazzo and Ramamohan Paturi around 1999, makes a sharper claim than P ≠ NP: no algorithm solves 3-SAT in 2^o(n) time, meaning no algorithm is subexponential in the worst case.[^3] P ≠ NP only says there is no polynomial algorithm. ETH says the exponential is real.

That sharpness is why ETH matters outside complexity theory. Hundreds of papers in graph algorithms, databases, computational biology and geometry use it as a starting assumption. They reduce 3-SAT to their own problem and conclude: if your problem had a subexponential algorithm, so would 3-SAT, and ETH forbids that. Those are the "conditional lower bounds" you see in the literature, and ETH is the load-bearing wall under many of them.[^4]

OpenAI's preprint claims to knock the wall down. As summarized on alphaXiv, it describes a deterministic algorithm that counts satisfying assignments of any k-CNF formula, for fixed clause width k, in time roughly (n+m)^O(1) · 2^(n/(log n)^(1/2+o(1))) and polynomial space.[^5] Counting solutions also decides satisfiability, since a count of zero means unsatisfiable. If the bound holds, it is subexponential, and ETH is false.

The bound is also underwhelming in practice, which is a useful thing to see early:

import math

# How much does a 2^(n / sqrt(log2 n)) bound save over brute-force 2^n?
# Constants and lower-order terms are ignored: this is intuition, not a benchmark.
for n in (1_000, 1_000_000, 1_000_000_000):
    saved = n / math.sqrt(math.log2(n))
    print(f"n={n:>13,}: 2^n vs 2^{saved:,.0f}  (exponent shrinks {n/saved:.1f}x)")

n=        1,000: 2^n vs 2^317  (exponent shrinks 3.2x)
n=    1,000,000: 2^n vs 2^223,990  (exponent shrinks 4.5x)
n=1,000,000,000: 2^n vs 2^182,887,335  (exponent shrinks 5.5x)

A million-variable formula still needs 2^223,990 steps. Asymptotically that is a different universe from 2^n. Practically, SAT solvers on real inputs are not about to be replaced.

Three Claims, Three Levels of Evidence

ETH was the headline, but OpenAI announced three results together. Here is where each stands, according to the reporting I could verify:[^6]

| Result | The claim | What's public | Who is checking | |---|---|---|---| | Computer science | ETH is false | Natural-language proof and a Lean file | Impagliazzo, Paturi and Ryan Williams | | Harmonic analysis | Local smoothing conjecture holds in every dimension; reportedly implies Kakeya and Stein's restriction conjecture | Write-up and Lean proof in a public repository | No verifiers named; OpenAI advised releasing the raw output | | Physics | Existence proof for certain 4D gauge theories including QCD, with pure Yang-Mills as a subproblem | Nothing released | A group led by David Gross, which is holding the artifacts and will write its own account |

Two caveats on the table. First, outlets disagree on details: some describe the physics result as QCD, others as Yang-Mills, and the Kakeya implication appears in some accounts and not others. I could not reach OpenAI's own announcement, so treat every secondary summary with caution, including this one.

Second, the physics result is the weakest on evidence. A Lean formalization reportedly exists, but it is unreleased, so no outside party can check it. The ETH and local smoothing results are at least inspectable.

Early expert reaction is cautiously impressed. Alex Iosevich of Rochester called the harmonic analysis result a "historic development." Ryan Williams of MIT said a confirmed refutation of ETH would be a major development, while noting that verification was ongoing.[^7]

What Lean Checks, and What It Doesn't

"Formally verified in Lean" sounds like the end of the conversation. It is closer to the start.

Lean checks that a theorem follows from its definitions and axioms. It does not check that the definitions mean what the humans reading them think they mean. For ETH, the formalization has to encode what "3-SAT," "subexponential time" and "running time" mean: the computational model, how input is represented, how steps are counted. A proof can be perfectly valid about the wrong thing.

Here is an exaggerated version of the failure mode:

-- Illustrative only; not from OpenAI's repository.
-- A definition with a bug: it is trivially true of everything.
def SubexponentialTime (f : Nat → Nat) : Prop := True

-- Lean accepts this happily. The proof is valid; the statement is meaningless.
theorem solver_is_subexponential (f : Nat → Nat) : SubexponentialTime f := trivial

Real formalization errors are subtler than True. They look like an off-by-a-log in a runtime definition, or a computational model that is quietly more powerful than a Turing machine. Catching them requires an expert reading the definitions, which is exactly what the Impagliazzo, Paturi and Williams group is doing.

There is one early discrepancy worth watching. One report says the Lean file gives a slightly different subexponential bound than the preprint.[^8] That could be a harmless version mismatch, a typo, or a sign that the informal and formal arguments differ. It is the kind of thing you only notice when someone is reading both.

What Changes If It Holds

Even if the proof survives, the consequences are narrower than the headlines suggest.

• P vs NP is untouched. A subexponential algorithm is still not a polynomial one. OpenAI does not claim otherwise.
• Cryptography is not directly affected. RSA does not depend on ETH, and a subexponential bound with a weak exponent says little about practical attacks.
• Conditional lower bounds need an audit. The theorems stay logically valid as "if ETH then X" statements. But the conclusions they were cited for, that a problem is hard, lose their footing. Each needs a check on whether it survives under a weaker assumption.
• Practical SAT solving is unchanged. As the example above shows, an asymptotic win that only divides the exponent by a square root of a logarithm is invisible at real input sizes.

The more interesting downstream effect is on the field's conditional-hardness toolbox. If ETH falls but SETH-style assumptions are claimed to fall with it, as the preprint's body reportedly says, a lot of fine-grained complexity results lose their stated basis at once.[^5]

Counterpoints: Reasons for Patience

This is a preprint, not a result. Nothing here has been peer reviewed. OpenAI itself calls the materials "raw research data" and says it is not seeking academic credit.[^8]

False alarms have happened. A 2021 arXiv preprint claimed to refute the counting version of ETH. It did not become consensus.[^8] A refutation of something this entrenched deserves a high prior of error, even from a strong system.

Who gets to check matters. OpenAI chose the expert groups that received each result. The company acknowledges the trade-off: outside experts help turn AI output into understanding, but picking the first reviewers shapes who is involved first.[^9] The math and CS groups made the AI-produced data public immediately; the physics group delayed release so it could write its own interpretation.

Withheld artifacts can't be falsified. A claim whose proof only one committee has seen is a claim you take on trust. That is a defensible choice for a result this large, and a poor basis for a headline.

The pattern is now familiar. A recent Anthropic biology announcement drew complaints that its significance was overstated.[^9] Labs have an incentive to announce discoveries, and verification is slower than a press cycle. The right default is to wait for the checkers.

The Takeaway

• ETH is under review, not refuted. The Exponential Time Hypothesis claim is a non-peer-reviewed preprint plus a Lean file. The researchers who proposed ETH are checking it and have said not to read their involvement as endorsement.
• Lean verifies logic, not meaning. The remaining work is confirming the formal definitions match the real problem. That is human expert labor and it takes time.
• The three claims are not equally checkable. ETH and local smoothing have public artifacts. The physics result has none, so it cannot be independently assessed yet.
• Even if true, it's narrow. No P vs NP, no broken cryptography, no faster SAT solver. The impact is on which hardness results rest on a now-weaker foundation.
• The real story is the verification bottleneck. AI can now produce proofs faster than the community can read them. How labs release, and who gets to check, is becoming as important as the proofs themselves.

---

Footnotes

[^1]: "The Exponential Time Hypothesis Is False," preprint attributed to OpenAI, v1 dated October 26, 2026. See the summary page on alphaXiv. [^2]: Statement by Russell Impagliazzo, Ramamohan Paturi and Ryan Williams, as reported by Xenospectrum. [^3]: ETH background and attribution from El Solitario. [^4]: Conditional lower bounds that rely on ETH, as described by El Solitario. [^5]: Algorithm and bounds as summarized on alphaXiv. The summary page is secondary; the proof itself should be consulted directly. The page says the body also claims to refute #ETH, SETH, Gap-ETH and NSETH, while the abstract names only ETH. [^6]: Table assembled from ExplainX, MindStudio and Al Jazeera. These outlets disagree on some details, noted in the text. [^7]: Reactions from Alex Iosevich and Ryan Williams as reported by Al Jazeera. [^8]: Lean-versus-paper bound discrepancy, "raw research data" wording and the 2021 preprint, all as reported by Xenospectrum. [^9]: Shepherd process and release trade-off, plus the Anthropic comparison, per Al Jazeera.

---

Tags: openai, mathematics, complexity-theory, formal-verification, lean