OpenAI reports an AI-generated refutation of the Exponential Time Hypothesis
On 26 October 2026 OpenAI announced three results produced by its internal models, two of which it released publicly with machine-checked proofs. The first is a claimed refutation of the Exponential Time Hypothesis, proposed by Russell Impagliazzo and Ramamohan Paturi in 1999, which holds that Boolean satisfiability requires exponential time in the worst case; OpenAI says the natural-language proof was produced on 16 October and formalised in Lean the following day. The second is a proof of Christopher Sogge's 1991 local smoothing conjecture in every dimension, which OpenAI states also settles the Kakeya and Stein restriction conjectures, with a 59-page manuscript dated 25 October and a Lean formalisation posted to GitHub. OpenAI handed verification of the complexity result to a group led by Impagliazzo, Paturi and Ryan Williams, and said it is not seeking academic credit for the work.
Why It Mattered
The complexity claim, if it survives review, removes a foundation that a large body of theoretical computer science rests on. Hundreds of papers in graph theory, databases, computational geometry and computational biology derive hardness results conditionally on the Exponential Time Hypothesis; refuting it invalidates the conditional framing of those results rather than the problems themselves. The claimed algorithm is subexponential asymptotically but far too slow to be used, and it does not establish that P equals NP, so cryptographic assumptions in deployed systems are untouched. Complexity theorist Scott Aaronson wrote on 26 October that students brought him the news, a measure of how quickly it travelled through the field. Beyond the mathematics, the announcement is a record of how frontier labs were learning to publish machine-produced proofs. Three features are worth preserving: Lean formalisation as the trust mechanism in place of peer review; the appointment of outside expert groups, including the authors of the conjecture being attacked, to shepherd and verify; and the lab's declaration that it would not claim academic credit. These arrangements emerged after earlier disputes in 2026 over AI-attributed results in fluid dynamics and over the mass publication of model-generated manuscripts. The entry records a dated claim backed by machine-checkable artifacts, not a settled theorem: as of the announcement, no independent group had completed verification of either result. That distinction is itself part of the history, because the period when AI systems began producing proofs faster than communities could check them is the condition this announcement documents.
Who Built It
OpenAI
Applications
- Mathematics
- Theoretical Computer Science
- Automated Theorem Proving