What OpenAI has actually announced
OpenAI’s public repository contains an AI-produced claim that the Exponential Time Hypothesis, or ETH, is false. Its README describes the collection as research material rather than polished academic papers, with results at different stages of verification. The scope for this result reports a Lean formalization. This article explains the stated claim; it does not independently certify the proof.
The useful reader question is narrower than whether AI has made difficult computing problems easy: what barrier would this result remove, and what would remain difficult? A small Boolean puzzle helps separate those questions.
The thumbnail’s branching paths and green shortcut are an editorial illustration. They are not a diagram of the proposed algorithm or a measured speed comparison.
A solution can be easy to check and hard to find
Imagine three switches, A, B and C, each either on or off. A rule can require at least one of three conditions to hold:
- A is on, or B is off, or C is on.
- A is off, or B is on, or C is on.
- A is on, or B is on, or C is off.
Each line is a clause. The whole puzzle requires every clause to pass, using one consistent setting of the switches. With all three switches on, each line has at least one true condition. With all three off, each line also passes: the first two contain an off condition, and the third contains C being off.
Finding one working setting answers the satisfiability question. Counting asks how many settings work. For this particular example, each clause rules out one different setting, leaving five of the eight possibilities. Try listing them: the rejected settings are off/on/off, on/off/off and off/off/on.
Checking a supplied setting requires reading the rules. Searching by trying every setting instead gives 2^n possibilities for n switches. This brute-force count describes one method, not a proof that every algorithm must take that long.
ETH concerns the growth rate
The survey by Lokshtanov, Marx and Saurabh defines ETH through the complexity of 3-CNF satisfiability, the family of problems illustrated above. In accessible terms, the hypothesis rules out a general algorithm with subexponential dependence on the number of variables, allowing polynomial factors in input size.
Merely changing 2^n into 1.1^n would not refute it. Both have an exponent proportional to n. Subexponential growth means the exponent becomes a vanishing fraction of n as n increases. The distinction concerns arbitrarily large inputs and worst-case guarantees; it does not tell us how long a particular puzzle will take today.
A smaller exponent can still be enormous
Consider the hypothetical running time 2^(√n). At one million variables, the exponent would be 1,000. That is subexponential growth, yet 2^1,000 steps would be far beyond a usable calculation. This is our arithmetic illustration, not OpenAI’s stated bound.
P vs NP asks whether problems whose proposed solutions can be checked in polynomial time can also be solved in polynomial time. A polynomial bound has a fixed power of input length, such as its square or cube. Being subexponential does not imply such a bound: 2^(√n) eventually exceeds every fixed power of n.
Consequently, a subexponential SAT algorithm could refute ETH without settling P vs NP. Nor does a theoretical improvement specify the constants, implementation costs or input sizes at which it becomes useful. Those require separate analysis and measurements.
Read the scope before comparing the bounds
OpenAI’s published formalization scope describes exact counting for canonically encoded k-CNF formulas, for each fixed clause width k of at least two. Three is included. Fixed width means choosing k first; it does not promise the same guarantee when clause width grows freely with the input.
The scope gives a deterministic algorithm, subexponential dependence on variable count, polynomial overhead in encoded input length, and polynomial space. Space measures memory use rather than running time. Exact counting returns a number; it does not require printing every satisfying assignment. A positive count answers yes to satisfiability, and zero answers no.
The document distinguishes the formalized bound from a sharper October 25 manuscript bound. Both are described as subexponential, but their logarithmic factors differ. They should not be reported as the same quantitative theorem.
A target statement is not its proof
The linked comparator statement specifies a machine, its input encoding, its exact answer and its time and space bounds. Its theorem ends with sorry, Lean’s placeholder for a missing proof. OpenAI links this as the statement against which the separate formalization is compared. That file alone establishes neither a successful proof nor a failure of the separate proof.
The Lean reference on proof validation explains why assumptions and meaning need their own scrutiny. A proof may depend on an unfinished result elsewhere; inspecting its axioms can reveal that dependency. Checking that a formal proof follows is also distinct from checking that the encoded statement means what the headline suggests.
Our earlier article on AI-generated software proofs develops that distinction for executable programs. Here the specific issues are the SAT input representation, the computation model and the resource bounds. We inspected the public scope and comparator; we did not rebuild the separate Lean proof.
What would change for other algorithms?
The ETH survey derives lower bounds by reductions: a sufficiently fast algorithm for another problem would yield a forbidden fast SAT algorithm. If ETH fails, a theorem conditional on ETH can remain logically correct while losing its justification as an unconditional limit.
That does not automatically produce a useful algorithm for every affected problem. The direction of a reduction and the size of the translated input still matter. The research question becomes which barriers can be supported by other assumptions, and which apparent limits can now be challenged constructively.
