The exponential time hypothesis (ETH) asserts an exponential lower bound for deterministic algorithms deciding 3SAT. Let 
count the variables and 
denote the input length, and use 
for big-O notation, so that
denotes a factor bounded by a fixed power of 
. Formally, ETH asserts that there is a constant 
such that no deterministic algorithm decides 3SAT
in time
 |
(Impagliazzo and Paturi 2001). In particular, it rules out a running time of 
,
where 
denotes a quantity whose ratio to 
tends to 0 (little-o
notation).
A 3SAT instance is a conjunctive normal form formula with at most three literals per
clause. More generally, 
-SAT allows at most 
literals per clause.
Equivalently, for each fixed 
, there are constants 
and 
such that no deterministic algorithm
solves 
-SAT
with at most 
clauses in time 
(Impagliazzo and Paturi 2001, Impagliazzo
et al. 2001). Thus the hypothesis distinguishes among superpolynomial
running times, rather than merely asserting that 3SAT
is not solvable in polynomial time. ETH implies
a negative answer to the P versus NP problem,
but the converse is not known.
OpenAI (2026a) reported a deterministic algorithm that, for each fixed 
, counts the satisfying assignments of a conjunctive
normal form formula with at most 
literals per clause.
In the bound below, 
is the number of variables, 
is the number of clauses, and 
is big-O notation whose
implicit constants and asymptotic thresholds may depend
on the fixed parameter 
, but not on 
or 
. The algorithm uses polynomial
space and has bit complexity
 |
The documented Lean bound instead has exponent 
, which is also 
. Either bound would refute ETH, but neither would establish
that P equals NP. An internal OpenAI model supplied the reported proof
and Lean formalization. Impagliazzo et al. (2026) invited community examination
of the OpenAI claim and explicitly distinguished their involvement from certification
of the proof. As of Oct. 28, 2026, independent mathematical
confirmation of the claim had not been reported.
Claude (2026) reported a separate deterministic algorithm for counting satisfying assignments of 
-SAT formulas in time 
for each fixed 
. The accompanying Lean statement includes this bound
on a deterministic Turing machine. It covers formulas
with 
variables and at least two clauses,
with no repeated clauses and every variable
occurring. An internal research Claude model at Anthropic discovered the algorithm,
and AI models wrote its formalization. As of Oct. 28, 2026, the formalization
had passed the project's automated checks, but independent mathematical confirmation
of this claim had not been reported.
Time Algorithm for 3-SAT." Oct. 26, 2026.
-SAT." J. Comput. Syst. Sci. 62, 367-375,
2001.