OpenAI said on October 26 that its system proved the Exponential Time Hypothesis (ETH) false, a result it says was verified in Lean. OpenAI says an internal model found the disproof on October 16 and the company checked it in Lean the next day. It’s a claim, not an accepted result, and the details matter.
What ETH is. It’s a 1999 conjecture by Russell Impagliazzo and Ramamohan Paturi that the 3-SAT problem can’t be solved in time that grows slower than exponentially. In plain terms, it’s the belief that some hard problems can’t be solved much faster than trying huge numbers of possibilities. Hundreds of computer science papers rely on it when arguing that problems in areas like graph theory, computational biology, and databases are hard. A genuine disproof would shake the assumptions behind a lot of that work.
What OpenAI claims. The manuscript describes a deterministic algorithm that exactly counts satisfying assignments of fixed-width CNF formulas in subexponential time and polynomial space, and says the 3-SAT case refutes ETH. OpenAI says an independent working group led by Impagliazzo, Paturi, and Ryan Williams will examine and explain the proof, and that the materials were made public immediately at the group’s request.
The experts are not endorsing it yet. The three researchers say their role in reviewing the work is not an endorsement, and that the claim needs careful independent scrutiny before it’s accepted. Daily.dev notes that the claim remains pending expert review.
The gap between the claim and the checked result. Lean is a proof assistant that mechanically checks whether a stated theorem follows from its definitions. OpenAI’s own Lean scope note, as described in the supplied materials, says the formalized result establishes subexponential-time exact counting and SAT for canonically encoded fixed-width CNF inputs, and distinguishes that from the manuscript’s sharper stated bound. So “verified in Lean” shouldn’t be read as “Lean proved every version of the claim.” The formalized statement is narrower than some of the prose around it.
What outside review has to settle. Reviewers will need to check whether the paper’s definitions match the formal ones, whether the canonical-encoding restriction changes what the theorem really covers, and whether the reduction from exact counting to the 3-SAT consequence holds up. OpenAI itself says practical algorithms will require significant further research, so even if the result stands, it wouldn’t be an immediate speed-up for real software.
Context. The ETH claim was one of three AI-produced results OpenAI announced on October 26, alongside a proof of the local smoothing conjecture and an existence proof in quantum field theory. Each has a different review path.
Bottom line: OpenAI has attributed a very large complexity-theory claim to its system and released materials for inspection, including a Lean formalization. Its own scope note shows the machine-checked statement is narrower than the manuscript’s strongest bound, and the original ETH authors are reviewing without endorsing. Until that review reports back, “ETH is false” is an unconfirmed claim, not an established result.
