OpenAI's AI disproved the Exponential Time Hypothesis: here's what that actually means
On 26 October 2026, OpenAI published an AI-generated disproof of the Exponential Time Hypothesis, verified in Lean, with open data and community funding.
On 26 October 2026, OpenAI published what it describes as an AI-generated disproof of the Exponential Time Hypothesis (ETH), one of the most widely relied-upon assumptions in theoretical computer science. The disproof comes with a formal proof verified in Lean, all raw data made publicly available, and a commitment to fund a community conference on the implications. Independent verification is under way, led by the very researchers who proposed ETH in the first place.
This post focuses specifically on that computer science result, because it is the one with the most direct and long-lasting consequences for how we think about computational difficulty.
What is the Exponential Time Hypothesis?
The ETH was proposed in 1999 by computer scientists Russell Impagliazzo and Ramamohan Paturi at the University of California, San Diego. Put simply, it asserts that certain hard problems, most famously Boolean satisfiability (SAT), cannot be solved meaningfully faster than brute force in the worst case. More precisely, it says no algorithm can solve k-SAT in sub-exponential time.
That might sound abstract, but ETH has become load-bearing scaffolding for a huge portion of theoretical computer science. Hundreds of papers across graph algorithms, computational biology, database query optimisation, and computational geometry use ETH as a conditional hardness assumption. The logic runs: “We cannot prove this problem is hard outright, but if ETH holds, then our lower bound follows.” Researchers have been building on that foundation for more than two decades.
What OpenAI’s model found
On 16 October 2026, an internal OpenAI model produced a natural-language disproof of ETH. The formalisation in Lean, a proof assistant that checks each logical step the way a compiler checks code, was completed the following day. The paper and the Lean proof are publicly available on GitHub.
The technical result is a deterministic algorithm that exactly counts the satisfying assignments of fixed-width CNF formulas in sub-exponential time and polynomial space. The 3-SAT case is enough to refute ETH. The time improvement is modest in practical terms: the algorithm gains roughly a square-root-of-log-n factor in the exponent. OpenAI is explicit that more study is needed before any concrete algorithmic improvement follows from this.
Who is checking it
A verification group has been formed, led by Impagliazzo and Paturi alongside Ryan Williams of MIT. The fact that Impagliazzo and Paturi, who originally proposed ETH roughly 25 years ago, are now checking a claimed disproof of their own conjecture is not lost on anyone.
They have been clear about the limits of their role. In an open letter, the group wrote: “Our involvement should not be taken as certification of the claim.” Williams confirmed on X that the group signed no non-disclosure agreements and will not be paid. OpenAI says participants will receive recognition for any expository work they produce, but the company is not seeking academic credit for the discovery itself.
OpenAI has also made all raw data publicly available and committed to funding a conference so the broader community can examine and discuss the result. The company contributed $5 million to the Simons Foundation on 6 October 2026 to support workshops, conferences, and special programmes on understanding AI-produced results, and that funding applies here.
What this does not mean
Two things worth being clear on, because the headlines can imply more than the result actually delivers.
First, this does not solve P vs. NP. OpenAI president Greg Brockman noted that P still probably does not equal NP. The ETH result is a narrower, more technical finding about one specific hypothesis. Disproving ETH removes a conditional hardness assumption; it does not collapse the boundary between tractable and intractable problems.
Second, if the disproof is confirmed, it will not make currently hard problems suddenly easy to solve. The sub-exponential improvement in the proof is theoretically significant but practically tiny. Researchers will need to revisit assumptions built on ETH, but that is a process of academic reassessment, not an overnight shift in what computers can do.
What this means for you
If you work in or around theoretical computer science, the implications are real even if indirect. A confirmed ETH disproof means:
Conditional lower bounds need reassessment. Papers that use ETH to argue “this problem cannot be solved faster than X” will need to re-examine their foundations. That does not make those results wrong, but it does remove one of the props they rest on.
Algorithmic research opens up. If the hardness floor was lower than assumed, there may be room for faster algorithms in areas where researchers stopped looking because ETH told them not to bother.
The verification process itself matters. OpenAI’s approach here, publishing raw output, funding independent verification with no NDAs, and explicitly declining academic credit, is a deliberate attempt to model how AI-generated scientific results should be handled. Whether that process proves sufficient for a result of this magnitude is something the community will be watching closely.
For everyone else, the honest answer is: not much changes yet. This result needs to survive expert scrutiny before the field restructures around it. The Lean verification adds confidence, but as OpenAI acknowledges, formal proof checking is not the same as full peer review. The community conference and open data release exist precisely because one formal proof and one verification group are not enough for a claim this consequential.
How OpenAI is approaching the release
OpenAI’s framing is deliberate. It describes the AI outputs as “a form of raw research data” rather than finished papers, and it has experimented with different release strategies for the three results it announced on 26 October 2026. For the ETH result specifically, it formed an external group of collaborators to explain the result while making the AI output publicly available for anyone to examine and build on.
That approach sits somewhere between traditional pre-print publication and fully open release. It acknowledges that a result this significant requires more than a GitHub repository and a Lean file, while still making the underlying material accessible before any official academic imprimatur.
Whether this process works, and whether the disproof holds, are questions that will play out over the coming months. The raw materials are there. The verification group is assembled. The field now has the uncomfortable and genuinely interesting job of finding out whether one of its foundational assumptions was wrong all along.