OpenAI Says Its Model Disproved the Exponential Time Hypothesis, Checked in Lean

TL;DR

On October 26, OpenAI announced three results from its unnamed internal model and pushed two of them, with Lean proofs, to the public openai/math repository. The one that will be argued over is a 67-page paper titled "The Exponential Time Hypothesis is False": a deterministic algorithm that counts the satisfying assignments of any k-CNF formula in 2^(n/(log n)^(1/2+o(1))) time and polynomial space. If the statement in the accompanying Lean file says what OpenAI thinks it says, a conjecture that hundreds of hardness results have rested on since 1999 is gone. Russell Impagliazzo and Ramamohan Paturi, who proposed ETH, and MIT's Ryan Williams will run an open, unpaid examination, and their letter says their involvement "should not be taken as certification of the claim." The same drop claims Sogge's local smoothing conjecture in every dimension, which would settle Kakeya, plus an existence proof for QCD and pure Yang-Mills that a group led by Nobel laureate David Gross has chosen to keep off GitHub for now.

What landed in the repo

The repo's history file for October 26 lists two new manuscripts, both with Lean formalizations, plus a Lean proof added for the earlier Hodge-conjecture-for-CM-abelian-varieties claim. The catalogue now holds 721 manuscripts in 373 families, one fewer than the 722 AI Bacon covered on October 7: OpenAI withdrew three papers over a sign error that same day, revised 14 others, and has now added two. The README still calls the collection "raw research data" and still names no model.

OpenAI's own dates for the new work:

• September 9: a natural-language proof of pure Yang-Mills existence. September 18: the QCD proof. October 16: the Yang-Mills Lean formalization finished.
• October 16: the ETH disproof. October 17: formalized in Lean. The PDF is dated October 17, revised October 25.
• October 18: local smoothing in every dimension. October 19: formalized in Lean.

The ETH claim, in plain terms

The Exponential Time Hypothesis, from Impagliazzo and Paturi's 1999 paper on the complexity of k-SAT, says 3-SAT on n variables needs 2^(Ω(n)) time. You may improve the base of the exponential but you never escape its shape. Brute force is 2^n. S. Liu's 2018 deterministic algorithm, which the Wikipedia SAT page cites at O*(1.32793^n), is still c^n for a c above 1. ETH says every algorithm is.

OpenAI's Theorem 1.1 breaks the shape. For every fixed k ≥ 2, the algorithm computes the exact number of satisfying assignments of a k-CNF on n ≥ 20 variables and m clauses in (n+m)^(O_k(1)) · 2^(O_k(n log log n / √log n)) bit operations and (n+m)^(O_k(1)) bits of space; at fixed clause density the exponent is O(n/√log n). Williams summarized it as 3-SAT in "about exp(n/(log n)^{1/2+o(1)}) time," and Scott Aaronson's blog gives the same rough shape, exp(n/√log(n)). Since testing whether the count is positive decides satisfiability, 3-SAT runs in 2^(o(n)) time and ETH is false.

Think of a toll that has always been a fixed fraction of your odometer reading. The new algorithm's toll is your odometer divided by a number that keeps creeping up the farther you drive. On any trip you can afford, the difference is invisible. In the limit, it is a different road, and complexity theory is about the limit.

The paper is careful about what does not follow. Page 2 notes that 2^(o(n)) bounds "do not transfer under general polynomial-time reductions," so the result "does not imply that general NP problems admit subexponential time algorithms." It does give 2^(o(v)) counting of independent sets and proper q-colorings on v-vertex graphs, and subexponential approximation for Max-k-SAT. Appendix C uses Williams's 2013 theorem, that a faster 3-SAT algorithm implies circuit lower bounds, to conclude that E^NP has no linear-size circuits, and adds that this "does not assert a superpolynomial circuit lower bound for NP." Your SAT solver is unaffected this week: the constants hide inside O_k(1), the theorem is stated for n ≥ 20, and nobody has implemented it.

What Lean actually checked

The formalization is catalogued as one target, OAI.Algorithms.SubexponentialSAT.SqrtLogSpace.exact_count_and_sat, verified with Comparator, the Lean FRO tool that has since been merged into Lean core as lake check. Comparator takes a challenge file in which the theorem is stated and the proof is a hole, then confirms three things about the solution: it proves the identical statement, it uses no axioms beyond propext, Quot.sound and Classical.choice, and the Lean kernel accepts it. The challenge file for this result, SubexponentialSAT.lean, defines literals, clauses, CNFs and their count from scratch, encodes a formula as a bit string, and specifies a multitape Turing machine whose step count is the time bound. The SubexponentialSAT directory behind that single declaration holds 3,977 Lean files and 35.5 MB of source. The local smoothing proof has six Comparator targets and 73 files.

Lean checks a proof against its statement the way a compiler checks a program against its type signature. It will catch any gap in the argument, and it has no opinion on whether the signature describes the function you wanted. The working group's real job is the challenge file: do the machine model, the input encoding and the time bound in SubexponentialSAT.lean add up to the sentence "3-SAT is in 2^(o(n)) time"? The 35 MB of proof is the part a kernel can vouch for.

The reviewers' terms

Williams posted that he, Impagliazzo and Paturi "have been asked to help organize an open and independent examination of this claim," that the group signed no NDAs and will not be paid, and that it asked OpenAI to publish all raw data for the result, PDFs and Lean source included, and to fund a conference for the research community. OpenAI agreed to both, and its announcement says so. The three wrote in an open letter, quoted by The Next Web: "Our involvement should not be taken as certification of the claim. A result of this significance requires careful, independent scrutiny." And: "If the claim is correct, it will change an important part of theoretical computer science." They also raised credit. When an AI finds a result first, recognition tends to go to whoever publishes first or owns the biggest tools, while the people who check and explain the work get less of it.

OpenAI describes the release as an experiment with three strategies, one per result. For the math result, publish the AI output and let researchers organize themselves. For the computer science result, form an external group and publish everything anyway. For the physics result, form a group and let it decide what to release. Four principles govern the groups: transparency with no NDAs, no academic credit claimed by OpenAI, recognition for the writeups the groups produce, and independence, meaning voluntary, unpaid and speaking only for themselves. OpenAI also points to a $5 million contribution to the Simons Foundation for workshops on AI-produced results.

Kakeya in every dimension, and QCD behind a Gmail address

The math result is the local smoothing paper, 59 pages. Christopher Sogge conjectured in 1991 that the worst-case focusing of a wave is short-lived, so averaging over a time window buys regularity you cannot get at a fixed instant. Guth, Wang and Zhang proved it in two spatial dimensions in 2019, and Wang and Zahl proved the three-dimensional Kakeya conjecture in 2025. OpenAI's paper claims local smoothing in every dimension n ≥ 2 through what the announcement calls a novel auxiliary partial differential equation. The abstract lists what falls out: the Bochner-Riesz conjecture, sharp bounds for Stein's square function, Fourier restriction for the sphere, paraboloid and cone throughout the interior of the conjectured range, local smoothing for Schrödinger, and the Kakeya and Nikodym maximal conjectures, so every Euclidean Kakeya set has full Hausdorff dimension. The October 6 release had claimed Kakeya in three and four dimensions with no Lean. This one carries Lean for six statements.

The physics result is the one nobody outside the group can read. OpenAI says its models produced a rigorous existence proof, building on Balaban's constructive approach, for interacting four-dimensional quantum field theories with gauge fields and fermions, including QCD and the simplest grand unified completion of the Standard Model. Pure Yang-Mills existence comes along as a sub-result, which is part of the Clay Yang-Mills and mass gap Millennium Prize problem. David Gross, who shared the 2004 Nobel for asymptotic freedom, leads a group with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov, and they have chosen to write it up themselves before any AI artifact ships. All enquiries go to [email protected], which is the most 2026 sentence in this article.

Why a builder should care

Hundreds of papers derive conditional lower bounds from ETH: no n^(o(k)) algorithm for k-clique, no subexponential algorithms for a long list of graph and database problems. Every one of those is now conditional on a hypothesis a 67-page PDF says is false. Nothing in them becomes wrong, since "if ETH then X" survives a false ETH, but the guarantees stop meaning anything, and the search for faster exact algorithms in those areas reopens. The 622-point Hacker News thread spent its first hours relearning what subexponential means; Aaronson's reaction was "Even as we struggle to digest the previous courses, the endless buffet continues!"

What changed most is the release format. The model is still unnamed. The paper is still a PDF the company calls data. The thing that makes this different from a press release is a challenge file anyone can run through lake check, plus three complexity theorists with no NDA and no paycheck who insisted the raw data be public before they would touch it. OpenAI has already retracted three papers from this repo for a sign error, which is a decent argument for the Lean-first part. If you want to audit the claim yourself, the repo's Comparator instructions are four lines long, and the file to read first is the challenge, not the proof.

Key Takeaways

• OpenAI claims a deterministic algorithm that counts k-CNF satisfying assignments in 2^(n/(log n)^(1/2+o(1))) time and polynomial space, which refutes the Exponential Time Hypothesis for 3-SAT.
• The disproof is dated October 16, was formalized in Lean on October 17, and shipped October 26 as a 67-page PDF plus 3,977 Lean files checked by Comparator against a public challenge statement.
• Impagliazzo, Paturi and Williams will run an open, unpaid examination. Their letter: "Our involvement should not be taken as certification of the claim."
• The result does not give polynomial-time 3-SAT or subexponential algorithms for NP in general, and no practical solver changes; it does yield subexponential counting for colorings and independent sets and a linear-size circuit lower bound for E^NP.
• The same release claims local smoothing in every dimension, settling Kakeya and Stein restriction, with Lean for six statements, and an unreleased existence proof for QCD and Yang-Mills held by a David Gross-led group.
• The repo now has 721 manuscripts in 373 families; three were withdrawn on October 7 for a sign error, so treat the unformalized ones as drafts.

Sources: OpenAI: Working with academic communities to build scientific understanding, The Exponential Time Hypothesis is False (PDF), Local smoothing for the Euclidean wave equation (PDF), openai/math history, openai/math formalization catalogue, SubexponentialSAT.lean challenge, leanprover/comparator, Ryan Williams on X, The Next Web, Shtetl-Optimized, Wikipedia: Exponential time hypothesis, Hacker News