oai-math-revised beta

Browse › Theoretical computer science › 378 Disproof of the Exponential Time Hypothesis

The Exponential Time Hypothesis is False

OpenAI · October 25, 2026

Notes Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Discussion

Edit NOTES.md · Existing issues · Source on GitHub

Contributions

Abstract

We give a deterministic algorithm for exactly counting the satisfying assignments of an arbitrary $k$-CNF formula. For every fixed $k\ge2$, on a formula with $n$ variables and $m$ clauses, our algorithm uses space polynomial in $n$ and $m$ and runs in time $(n+m)^{O_k(1)}2^{n/(\log n)^{1/2+o(1)}}$. Our algorithm refutes the Exponential Time Hypothesis (ETH), which postulates that deciding 3-SAT on $n$ variables requires $2^{\Omega(n)}$ time in the worst case.

If the PDF does not display here, open it directly: Open PDF.

Notes

Follow-up works

Constructive comments / reviews

  • McElveen, measurement_toy.py: In the toy's extension of Section 2.7 to $R=Q+1$, outside the paper's parameter regime, choosing the interpolation interval $\{0,\ldots,Q\}$ gives $M_0=I$ and no measurements, with replacement forms of degree up to $Q$; this illustrates the remark that a different form at each point "would generally cost degree $Q$" (run with --design aux --Q 3 --R 4).
  • oai-math-recheck, family 378: Independent re-check at openai/math 7ef5c0c, which the comparator run of 2026-10-26 predates: all 3,977 modules built, the theorem rests only on the three standard axioms, and the challenge and solution statements elaborate to identical constants, definition bodies included; this is not a comparator run.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-30) and not checked by a person. May be wrong or incomplete. Report an error.

Follow-up works

  • Anthropic (submitted by Jelani Nelson), A $2^{o(n)}$ Time Algorithm for 3-SAT (hexagon:2610.00577v1, 2026-10-27). An independent, concurrent claim of a deterministic $2^{o(n)}$-time algorithm for 3-SAT and #3-SAT, which its provenance note says was found by an internal Claude model and formalized in Lean 4. Its provenance statement says an internal OpenAI model independently and concurrently claims a similar result, and its reference list cites this preprint. [AI-generated per source]
  • Deep Bhattacharjee, Subexponential Weighted Counting and Exact Optimisation (hexagon:2610.00594v1, submitted 2026-10-28). Restates the preprint's $k$-CNF counting algorithm and claims an extension of it to sums of local weights in any commutative $\mathbb{Q}$-algebra, with applications including sparse Max-Cut and Max-$k$-SAT, the independence polynomial, Ising and Potts density of states, and decoding for sparse parity-check codes; Hexagon labels the text as mixed human and AI. [AI-generated per source]
  • Isaac Rudich and Louis-Martin Rousseau, Deterministic Factoring in Time $N^{o(1)}$ (hexagon:2610.00600v1, submitted 2026-10-28). Claims, with a Lean certificate, a deterministic machine finding the smallest prime factor of $N$ in $N^{o(1)}$ steps by counting divisors with prescribed leading bits; it cites this preprint for the counting engine but says it re-proves the part it needs and imports nothing from the ETH developments; the provenance statement says the ideas and Lean proof were generated by Claude Opus 5.5 and that the authors specified and audited the statement but did not read the proof. [AI-generated per source]
  • Xiaoyu Li (contributor), What Does the Refutation of the Exponential Time Hypothesis Mean for Learning Theory? (hexagon:2610.00613v1, submitted 2026-10-28). Uses this preprint and the Anthropic preprint as black boxes to derive speed-ups for learning when each example depends on few hypothesis bits, so its conclusions are conditional on the refutations; its provenance note says Claude Opus 5.5 produced the content. [AI-generated per source]

Comments and discussion

  • Scott Aaronson and commenters, Shtetl-Optimized, Podcasts about the Topic: Part II (comment thread) (blog, 2026-10-26). The post reports the claimed roughly exp(n/√log n) 3SAT algorithm, and in comment #17 Aaronson says the speedup concerns fixed-width k-SAT and gives nothing comparable for CircuitSAT or FormulaSAT. That comment answers asdf (#15), who asks whether general SAT reduces to 3SAT in subexponential time. Joshua Zelinsky (#2) notes that the bound does not beat the number field sieve for factoring or the best graph isomorphism algorithms and points to results known to be optimal under ETH, and Jonathan Baxter (#6) notes that the manuscript's exponent has one factor of log log n where the formalized bound has its square.
  • Hacker News, The Exponential Time Hypothesis Is False [pdf] (HN item 50251661, 2026-10-26). A thread with about 200 comments. It discusses whether the $2^{n/(\log n)^{1/2+o(1)}}$ bound survives polynomial-time reductions to other NP problems, whether the algorithm has any practical value, and whether the Lean check reduces the burden of verifying the paper.
  • Ryan Williams (@rrwilliams), post on X (2026-10-27). A thread explaining the claim for non-experts: if true, it gives faster algorithms for many other NP problems, and Williams says one of his first requests was for OpenAI to check that no existing cryptosystems are compromised, which "apparently" they are not.
  • Ryan O'Donnell (@BooleanAnalysis), post on X (2026-10-26). Says results assuming ETH do not fall, since they are efficient reductions from 3SAT that still work, and expects one of them could simplify the OpenAI proof.
  • B (@QuantumTumbler), post on X (2026-10-26). Says the qualitative $\mathsf{E}^{\mathsf{NP}}$ circuit bound needs only the Lean algorithm plus Theorem 6.1 of Williams's 2013 paper (cited by the manuscript), but the $n\sqrt{\log n}$ rate in Corollary 1.4 relies on the sparse bound and the JMV local reduction, neither formalized in Lean.
  • Ryan Williams (@rrwilliams), post on X (2026-10-29). Places the OpenAI algorithm in the class Williams calls "split and list", which reduces an NP problem to an exponentially large instance of a P problem, and in a follow-up post notes that it still brute-forces within pieces, giving this as the reason to expect further improvements.
  • Ryan O'Donnell (@BooleanAnalysis), post on X (2026-10-29). Replying to Williams, describes the OpenAI and Anthropic proofs as algebra: build matrices $A(t)$ with $A=A(0)$ whose permanents at $t=1,\ldots,\ell$ are easy because the matrices are structured, the Anthropic proof being a more awkward version with $\ell=2$.
  • edwardahirsch, comment on Lance Fortnow's The Exponential Time Refutation (blog comment, 2026-10-29). Suggests that a similar sublinear-exponent bound holds for fixed-linear-size CircuitSAT with respect to the number of variables, which would end upper bounds of the form $c^g$ in the number of gates, subject to checking the exact asymptotics.
  • Karthik Bhaskar (@kbhaskar_95), post on X (2026-10-27). Says both the OpenAI and Anthropic papers have general bound $2^{O(n\log\log n/\sqrt{\log n})}$, with $n/\sqrt{\log n}$ being the case of $O(n)$ clauses, and that the Lean files differ: Anthropic's states the paper's bound, while OpenAI's public file states the weaker $n(\log\log n)^2/\sqrt{\log n}$ exponent, which the post places in Section 6.4 of the manuscript.
  • Joshua Grochow (@joshuagrochow.bsky.social), post on Bluesky (2026-10-28). Says many results in papers that assume ETH can probably be "rescued" with minor changes, since the disproof is only by a tiny amount, and points to two CS Theory Stack Exchange questions (57311 and 57309) for discussion.

Formalization

Possibly relevant literature (found by the agent, not checked)

Digests and expositions

  • Ryan O'Donnell, Some exposition of "The Exponential Time Hypothesis Is False" (12 pages, 2026-10-26; shared on X on 2026-10-27). An LLM-assisted rewrite that aims to explain the main ideas more clearly, using some quantum language and specializing the argument to a simpler counting problem; the post adds the disclaimer "no idea if it's correct". [AI-generated per source]
  • Ryan O'Donnell, ETH False (lecture recording) (CMU graduate complexity class, YouTube, 2026-10-29). An 80-minute lecture which, according to O'Donnell's post, covers the main plan and the basic ingredients of the #3SAT result but not the full proof.
  • Mark Sellke, An Outline of OpenAI's $2^{o(n)}$-Time $k$-SAT Algorithm (slides, October 2026; announced on X 2026-10-28). Outlines the preprint's algorithm aiming at $2^{o(n)}$, and the announcement says that the skipped steps give a smaller power of $\log n$ in the exponent than the fully optimized algorithm.
  • Shiva Kintali, A simplified proof of ETH is false (22-page exposition, dated 2026-10-26). Explains OpenAI's proof as a family of deterministic $C_\varepsilon(n+m+1)^{c_\varepsilon}2^{\varepsilon n}$-time algorithms for fixed $\varepsilon>0$, combining sparsification, bounded occurrences, spectral replacement and rational interpolation, with manually expanded explanations and a worked example following interaction with Claude and ChatGPT. [AI-generated per source]
  • Scott Kominers (submitter), On counting satisfying assignments via polynomial separation (hexagon:2610.00574v1, 2026-10-27). A preliminary exposition of a qualitative form of the main result that separates the general counting procedure from the construction feeding it, and which the author calls "highly preliminary and heavily LLMathed". [AI-generated per source]
  • Ryan O'Donnell (@BooleanAnalysis), post on X (2026-10-28). A thread sharing a "still badly written" progression of ideas for #3SAT via sparse permanents in time about $2^{n/\sqrt{\log n}}$, with a post saying the key algebraic construction comes from elementary analysis of Boolean functions, a reply calling it "basically 100% the OpenAI one", and another saying the main "trick" is "stuck at sqrt(log n)" while new tricks of similar types remain an open question.

News and blogs

Elsewhere

Independent sites; their content is not reviewed here.

Cite

@misc{OAI:The-Exponential-Time-Hypothesis-is-False-October-25-2026,
  author = {{OpenAI}},
  title = {{The Exponential Time Hypothesis is False}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf}{OAI:The-Exponential-Time-Hypothesis-is-False-October-25-2026}},
  year = {2026}
}

Lean formalization

OpenAI provides Lean files for this family. The scope note, lean/docs/378.md, says which results they cover.

Each result is stated in a file in lean/ComparatorChallenges/. These files end in sorry on purpose: they only state the result. The proof is in a separate module, and Lean's comparator is the tool for checking that the module proves exactly what the statement file says.

Nobody has checked whether the Lean statements say what the paper claims.

Family 378: Disproof of the Exponential Time Hypothesis

For every fixed $k\ge2$, a deterministic algorithm counts the satisfying assignments of a $k$-CNF with $n$ variables and $m$ clauses in time $(n+m)^{O_k(1)}2^{n/(\log n)^{1/2+o(1)}}$. This yields superlinear circuit lower bounds for a language in $\mathsf{E}^{\mathsf{NP}}$ on infinitely many input lengths.

This is the only paper in this family.