OpenAI's model claims to refute the Exponential Time Hypothesis, with a Lean proof anyone can read

OpenAI says an unreleased internal model has refuted the Exponential Time Hypothesis, the conjecture that 3-SAT cannot be solved in time 2^(o(n)) on n variables. The claim arrived on October 26 alongside two others: a proof of Sogge's local smoothing conjecture in every dimension, which would also settle the Kakeya conjecture, and a mathematically rigorous existence proof for four-dimensional quantum chromodynamics that includes pure Yang–Mills existence, part of a Clay Millennium Prize problem.

Of the three, the ETH result is the one anyone can inspect today. The 67-page paper and a Lean formalization are in OpenAI's public openai/math repository. The physics materials are not: the outside group shepherding that result, led by David Gross, has chosen to write it up itself before anything is released.

What is claimed

ETH, proposed by Russell Impagliazzo, Ramamohan Paturi and Francis Zane, says there is some constant δ > 0 such that 3-SAT needs 2^(δn) time in the worst case. A great deal of fine-grained complexity rests on it: OpenAI's announcement says hundreds of papers use it for conditional hardness results.

The paper claims more than a decision procedure. For every fixed k ≥ 2 it gives a deterministic algorithm that exactly counts the satisfying assignments of a k-CNF formula with n variables and m clauses in (n + m)^(O_k(1)) · 2^(O_k(n log log n / √log n)) bit operations and polynomial space. With a linear number of clauses the exponent improves to O(n / √log n). Any running time of the form 2^(o(n)) contradicts ETH, so if the theorem holds, ETH is false.

The paper is careful about what does not follow. A 2^(o(n)) bound does not survive general polynomial-time reductions, so this is not a subexponential algorithm for every NP problem, and P vs NP is untouched. The direct corollaries are subexponential exact counting of independent sets, proper q-colorings and perfect matchings.

What the Lean proof actually checks

"Verified in Lean" can hide a lot, so the statement deserves a look. The challenge file is short and readable. It defines CNF formulas, their bit encoding and a primitive multi-tape machine model, built on Mathlib's Turing-machine tapes. The theorem exact_count_and_sat asserts that for each k ≥ 2 there is one fixed machine that, on any formula of width at most k, halts with the exact model count on one tape and the satisfiability bit on another; that it finishes within C · (input bits + 1)^d · 2^(A · ρ(n)) steps; and that it never touches more than polynomially many tape cells along the way.

The statement leaves little room for a definitional trick, such as a cost model that quietly makes exponential work free. The Comparator configuration allows only Lean's three standard axioms (propext, Quot.sound, Classical.choice). We read the statement and the configuration; we did not build the formalization ourselves.

One gap between paper and formal proof is easy to miss. The function the Lean theorem bounds is ρ(n) = n (log log n)² / √log n. The paper's main theorem uses the sharper n log log n / √log n, and the introduction notes that the rational-interpolation argument gives only the weaker ρ(n). The repository's formalization catalogue lists that weaker theorem for this paper. Either bound is 2^(o(n)), so the refutation does not depend on the difference. The sharper headline bound, as far as the catalogue shows, has not been machine-checked.

Subexponential, eventually

ETH is an asymptotic statement, and so is its refutation. Using natural logarithms, as the paper does, and setting the unknown constant A to 1, ρ(n) only drops below n once ln n exceeds roughly 5,500, which means formulas with more than about 10^2,389 variables. At n = 10^100, ρ(n) is still about 1.95n. The sharper paper bound overtakes n much earlier, around 0.7n at a million variables, but it hides constants of its own. The Lean theorem only says that suitable constants exist; it does not give their values.

That makes no difference to the mathematics. A conjecture that says "no 2^(o(n)) algorithm exists" is false the moment one exists, however slowly its advantage appears. It does mean the practical impact is close to zero for now, which OpenAI concedes when it says that turning theoretical advances into practical improvements "will require significant further research". The bigger effect is on theory: lower bounds proved conditionally on ETH, or on the stronger Strong Exponential Time Hypothesis, which implies it, lose their foundation.

Who checks it

Impagliazzo, Paturi and MIT's Ryan Williams will lead a group to verify and explain the result. Two of them proposed the hypothesis being refuted, and Williams has spent years connecting algorithms to lower bounds. At their request, OpenAI published the raw materials immediately and committed to funding a conference on the implications. OpenAI's stated principles for the collaborations include no nondisclosure agreements and no academic credit for the company.

Some caution is warranted by the repository's own history. Its README describes 721 model-generated manuscripts, produced from about 4,000 posed problems, of which roughly 42% of top-line results are formalized, and warns that unformalized results "could have issues". On October 7 OpenAI withdrew three manuscripts after a sign error broke an argument two of them depended on. The ETH and local smoothing results are both in the formalized minority. Lean rules out that kind of slip, as long as the formal statement means what the paper says. Here, the statement is short enough for a complexity theorist to read in an afternoon.

The other two results

The local smoothing paper claims Sogge's 1991 conjecture for the wave equation in every spatial dimension n ≥ 2, by way of a new auxiliary PDE. Guth, Wang and Zhang proved the two-dimensional case in 2019. From it the paper derives the Bochner–Riesz conjecture, the Kakeya and Nikodym maximal conjectures, and restriction estimates for the sphere, paraboloid and cone "throughout the interior of the conjectured range". The Lean formalization states several of these consequences separately, including that every Kakeya set in R^n has full Hausdorff dimension. OpenAI says the model produced the proof on October 18 and the Lean proof followed a day later. It released the output with no shepherding group, at the advice of the expert it consulted.

The physics claim is the largest and the least examinable. OpenAI says its models produced a natural-language proof of Yang–Mills existence on September 9 and of QCD on September 18, and that the Yang–Mills formalization finished on October 16. Those are OpenAI's statements; no proof or Lean code is public. Until the Gross group publishes, there is nothing to evaluate beyond the announcement itself.