OpenAI says one of its AI systems has disproved the Exponential Time Hypothesis, a 27-year-old assumption that underpins hundreds of computer science papers. The claim, announced on 26 October 2026, is extraordinary, and it is not yet confirmed: independent experts have begun checking it. One note first, because the internet has already mixed it up: this ETH is a computer science conjecture, not Ethereum.
What the Exponential Time Hypothesis says
Proposed in 1999 by Russell Impagliazzo, Ramamohan Paturi and Francis Zane, the hypothesis concerns a classic logic puzzle called 3-SAT, where the task is to decide whether true-or-false values can be assigned to variables so that every linked condition holds. ETH says no algorithm can solve it much faster than brute-force search in the worst case. Researchers have used it in hundreds of papers to argue that problems in graph theory, databases and computational biology are inherently hard.
What OpenAI claims
OpenAI says its system found a natural-language disproof on 16 October and that the result was formalised and checked in Lean, a proof-checking language, on 17 October. According to the company's paper, titled "The Exponential Time Hypothesis is false," the result is a deterministic algorithm that exactly counts the satisfying assignments of fixed-width logic formulas in subexponential time and polynomial space. OpenAI has published the AI-written proof, the 67-page manuscript and the Lean files in a public repository.
What it does and does not mean
If the result holds, some problems once assumed to need exponential time may have faster solutions. OpenAI itself cautions that finding practical speed-ups will take substantial further research, and reports describe the algorithm as impractical for real-world use for now. The paper does not claim that all NP problems can be solved in subexponential time, so the famous P versus NP question is unaffected.
Who is checking
OpenAI says a group led by Russell Impagliazzo and Ramamohan Paturi of UC San Diego, two of the original proposers, and Ryan Williams of MIT will verify and shepherd the work. The company agreed to publish all raw data for independent verification and to fund a conference on the implications. The Washington Times reported that Paturi's first reaction was surprise.
Reasons for caution
A Lean check is strong evidence, but not a complete guarantee. A recent preprint argued that the Lean version of OpenAI's earlier Navier-Stokes work did not faithfully match the natural-language proof it was meant to capture, and concluded that AI-written proofs translated into Lean still need normal peer review. Until the expert group reports, the Lean check is the only independent test the ETH claim has passed.
OpenAI also announced two other results the same day, a proof of the local smoothing conjecture in every dimension and an existence proof related to quantum chromodynamics, and has asked outside experts to examine each. Those claims remain under review too.
Why it matters
If it stands, this would be among the most significant results an AI system has produced in theoretical computer science. If it does not, it will become a case study in how to verify AI-generated mathematics. Either way, the careful, public verification process is the story to watch over the coming weeks.
Sources: OpenAI, "Working with academic communities to build scientific understanding" (26 October 2026); Washington Times; Quartz, citing Al Jazeera; Unite.AI; Technology.org; arXiv preprint on Lean autoformalisation.
