OpenAI says its model proved the Exponential Time Hypothesis false

OpenAI released a preprint on Monday claiming that 3-SAT, the classic hard logic puzzle, can be solved in subexponential time. If it holds, the Exponential Time Hypothesis (ETH) is false. You can read the paper and its Lean proof today, and an open check led by two of the conjecture's original proposers is just starting.

What changed#

Per OpenAI's post, "Surprisingly, our system has recently proved that the ETH is false, a result that was subsequently verified in Lean." OpenAI says its AI found the disproof on Oct 16 and formalized it in Lean on Oct 17. The repo history says, "The paper gives a deterministic algorithm that exactly counts satisfying assignments of fixed-width CNF formulas in subexponential time and polynomial space."

MIT professor Ryan Williams, one of the three people organizing the check, summarized the claim: "3SAT on n variables is in about exp(n/(log n)^{1/2+o(1)}) time". That beats 2^n brute force but is still far from polynomial.

The same post makes two more claims:

• Math: a proof of Sogge's local smoothing conjecture in every dimension, which OpenAI's post says resolves the Kakeya conjecture and Stein's restriction conjecture "in all dimensions". The repo history words the Stein part more narrowly: "Stein’s spherical restriction estimates throughout the interior of the conjectured range".
• Physics: an existence proof for four-dimensional theories including quantum chromodynamics. OpenAI calls pure Yang-Mills existence "part of" the Clay Millennium problem. Clay's page is titled Yang-Mills & the Mass Gap, and OpenAI's post doesn't mention a mass gap. The physics group "decided to hold off on releasing the AI-produced artifacts".

Per the post, the models produced the Yang-Mills proof on Sep 9 and the math proof on Oct 18. The ETH group is Impagliazzo, Paturi and Williams; the physics group is led by Nobel laureate David Gross.

Why it matters#

Williams says that if the claim holds, "a variety of other NP problems now all have faster algorithms as well", and that it "should make every computer scientist put at least a little more weight on the possibility of P = NP". OpenAI president Greg Brockman posted "p still probably doesn't equal np".

OpenAI's post notes ETH "has been used in hundreds of papers to derive conditional computational hardness results", so a lot of published work would need a second look.

Our read: the bigger shift is how the result is being checked. OpenAI's Oct 6 release posted raw model output. This one arrives with named outside reviewers, a public proof and a Lean check from day one, and OpenAI says "We do not seek academic credit" for it.

How to use it#

1. Read the preprint on GitHub.
2. Per the README, "The Lean library and formalization catalogue describe the available formal proofs, their associated papers, and verification configurations."
3. Follow the organizers' letter, which lists a feedback form and a public discussion site.

Reading prompt (ours, untested), with the PDF attached:

Read the attached paper.pdf. In plain language, explain what the main algorithm does, list each lemma the main theorem depends on in order, and mark any step where the paper skips an argument or where you can't follow it. Don't say whether the result is correct.

Good to know#

• The letter from Russell Impagliazzo, Ramamohan Paturi (both UC San Diego) and Williams says "Our involvement should not be taken as certification of the claim."
• On security, Williams wrote that he asked OpenAI to check that "no existing cryptosystems are compromised by the result. Apparently they are safe..."
• On real-world solvers, OpenAI says "turning theoretical advances into practical improvements, will require significant further research".
• Per 2/4 of his thread, the group signed no NDAs and gets no pay, and asked OpenAI to release the raw ETH data. They also asked OpenAI to sponsor a conference; Williams wrote, "They agreed to both."
• Not everyone likes the reviewer setup. The Verge reports OpenAI's own math advisory panel had just said "we recommend that AI companies do not adopt" the practice of picking who sees results first.
• OpenAI's math releases have been corrected before. On Oct 7 it withdrew three manuscripts after "a sign error" broke a key argument. We covered the debate over its Navier-Stokes paper on Monday.

Last checked: Oct 27, 2026, 6:20 to 6:25 AM ET. What changed: quote completeness and Williams "agreed to both" rebind after Editor FIX.

Sources#

• OpenAI: Working with academic communities to build scientific understanding (Oct 26, 2026)
• openai/math: The Exponential Time Hypothesis is False (preprint)
• openai/math: release history
• openai/math: README
• Impagliazzo, Paturi and Williams: Message to the TCS Community on ETH
• Ryan Williams on X: a claimed refutation of ETH (thread)
• Ryan Williams on X: the claimed 3SAT running time
• Ryan Williams on X: more weight on P = NP
• Ryan Williams on X: cryptosystems check
• Greg Brockman on X: p still probably doesn't equal np
• The Verge: OpenAI announces three big science discoveries
• Clay Mathematics Institute: Yang-Mills & the Mass Gap