OpenAI: "The Exponential Time Hypothesis is False"
A deterministic algorithm counts the satisfying assignments of a k-CNF in subexponential time, refuting ETH.
What was claimed: A deterministic algorithm counts the satisfying assignments of a k-CNF in subexponential time, refuting ETH.
What Lean states: exact_count_and_sat (OpenAI's SubexponentialSAT challenge, openai/math at 7ef5c0cc), Lean v4.34.1 — exact_count_and_sat: Proposition 6.4 bound n(log log n)²/√log n on OpenAI's multitape machine over unary words.
Prose only / the gap: Headline Theorem 1.1 exponent n·log log n/√log n; textbook ETH definition (bridged externally by Toledo).
Verification & replays: Toledo (Comparator 80 GiB, nanoda, leanchecker --fresh); Szeider (crossover reading). Not replayed by SeamCert.
What the public sources report
Every item below is attributed to the published paper, replay, or commentary that reported it.
| What the Lean proves | The weaker Proposition 6.4 bound, exponent n(log log n)²/√log n. The paper's headline exponent n·log log n/√log n rests on the prose proof alone, as OpenAI's Lean scope note says. [1][2] |
|---|---|
| Machine model | Its own multitape machine on Mathlib tapes; a separate machine for each k; space proved polynomial. [2] |
| Input encoding | A set of sets of literals written as a canonical sorted unary word. [2] |
| ETH in the Lean | Not defined in OpenAI's files. Toledo wrote a textbook ETH in Lean and proved that OpenAI's statement refutes it in OpenAI's own machine model. [2] |
| Kernel checks | Comparator with Lean's kernel, and nanoda, both accept; only propext, Classical.choice and Quot.sound. leanchecker --fresh exit 0 in 2,896 s. nanoda is off in OpenAI's shipped config and was switched on for the replay. [2] |
| Replay cost | Comparator peaked at 80 GiB of memory. [2] |
| Statement reading | "A correct statement of the intended result, for a weaker but still subexponential bound." [3] |
| Where it stops being brute force | The main-text algorithm is an exhaustive search on every input with fewer than 2^(10^10) variables; the Appendix D algorithm below 2^131071 variables and clauses. [3] |
Open specification seams (our reading)
Our reading of the sources above: the places where the formal Lean statement and the informal headline claim can still come apart.
- The step from OpenAI's machine and unary encoding to a textbook machine and encoding. Toledo reports it now proved in Lean through Hawkley's chain and a port to complexitylib's Lean, with the port and the Lean version seam declared.
- The sharper Theorem 1.1 bound is prose only.
- That any formal ETH is the textbook ETH stays a reading of a definition.
Footnotes & Sources
- Papex, "Has the ETH refutation been verified?" (31 October 2026)
- Carlos Toledo, "Two claimed refutations of the Exponential Time Hypothesis: what was decided, and what was only read"
- Stefan Szeider, "OpenAI's claimed refutation of ETH: exhaustive search below 2^131071" (Zenodo, 27 October 2026)
- OpenAI, "The Exponential Time Hypothesis is False" (paper and Lean, openai/math)
Sources read on 7 November 2026. Spotted an error or a newer independent replay? Write to [email protected].