The Exponential Time Hypothesis

For $k\ge3$ let $s_k$ be the infimum of the $\delta$ for which $k$ -SAT on $n$ variables can be decided in time $O(2^{\delta n})$ . Impagliazzo and Paturi (2001) formulated the Exponential Time Hypothesis: $s_3>0$ , that is, there is a $\delta>0$ such that $3$ -SAT cannot be solved in time $2^{\delta n}$ , so no $2^{o(n)}$ -time algorithm exists. With the sparsification lemma of Impagliazzo, Paturi and Zane (2001) it underlies tight conditional lower bounds across exact, parameterized and fine-grained complexity, and it is a strengthening of $\mathrm{P}\ne\mathrm{NP}$ . Is it true?

Result: Disproved(see note)
Status: Candidate (review pending)
AI contribution: AI-discovered
Method: Argument
Field: Computational complexity; satisfiability algorithms
Posed by: Russell Impagliazzo and Ramamohan Paturi, On the Complexity of k-SAT, J. Comput. Syst. Sci. 62(2) (2001)
Year posed: 2001
Years open: 25y
Solved: 2026-10-17
Model: Unreleased internal OpenAI model
Vendor: OpenAI
Collaborators: —
Verification: Lean-checked, statement unaudited
Publication: Announced
Collection: OpenAI math release (October 2026), version 4eaee87
Significance: 76 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Theorem 1.1: for each fixed $k\ge2$ a deterministic algorithm computes the number of satisfying assignments of a $k$ -CNF with $n\ge20$ variables and $m$ clauses in $(n+m)^{O_k(1)}2^{O_k(n\log\log n/\sqrt{\log n})}$ bit operations and $(n+m)^{O_k(1)}$ bits of space, and in $2^{O_{k,D}(n/\sqrt{\log n})}$ when $m\le Dn$ . Testing whether the count is positive decides $3$ -SAT in $2^{o(n)}$ time, refuting ETH (and hence SETH). The paper notes this does not give subexponential algorithms for all of NP, since $2^{o(n)}$ bounds do not survive general polynomial reductions. Corollaries: subexponential Max- $k$ -SAT approximation schemes, exact counting of independent sets, $q$ -colorings and perfect matchings in $2^{o(v)}$ time, and an $\Omega(n\log n)$ circuit lower bound for a language in $E^{NP}$ .

What the AI did

Produced by an unreleased internal OpenAI model as part of an OpenAI evaluation on open research problems. The manuscript is authored 'OpenAI' and names no human author. The release README says the manuscripts are best understood as raw research data rather than polished papers, and that unformalized results could have issues. The manuscript is dated 17 October 2026, revised 25 October 2026; OpenAI's announcement says the model found the disproof on 16 October and that it was checked in Lean the next day. The release history (26 October) says an independent working group led by Russell Impagliazzo, Ramamohan Paturi and Ryan Williams will examine and explain the proof, and that the materials were made public at the group's request. The release ships a Lean formalization and a Comparator configuration for the main theorem.

Verification

No independent mathematician has checked this yet. Checked here on 3 November 2026: the abstract, introduction and Theorem 1.1, read against ETH as defined in [IP01]. The proof was not refereed. Lean: lean/formalization.yaml lists OAI.Algorithms.SubexponentialSAT.SqrtLogSpace.exact_count_and_sat (SqrtLogSpace/Final.lean, comparator ComparatorChallenges/SubexponentialSAT.json, axioms propext, Quot.sound, Classical.choice). Its challenge statement was read in full: for each $k\ge2$ one fixed multi-tape machine over Mathlib Turing tapes, on a canonical unary-coded CNF of bit length $L$ , halts with the exact count and the SAT bit, in time at most $C(L+1)^d2^{A\,n(\log\log n)^2/\sqrt{\log n}}$ and visited space at most $S(L+1)^e$ . A 3-CNF has $L=\mathrm{poly}(n)$ , so this is a $2^{o(n)}$ deterministic 3-SAT algorithm: the headline, with no extra hypotheses, at a slightly weaker exponent than the paper's. GitHub code search over the solution folder found no sorry, native_decide or implemented_by, and only #print axioms lines for 'axiom'; the search does not index every one of its about 4,000 files. Not rebuilt here.

Sources

Submitted by VibeGene on 27 Oct 2026

The Exponential Time Hypothesis

What was actually shown

What the AI did

Verification

Sources

Discussion