AI Proved What?

Episode 378, October 2026

The Exponential Time Hypothesis is false?

An AI preprint claims to count k-SAT solutions in subexponential time

Covers result 378 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

5:43. English captions available. The video loads from YouTube when you press play.

Versions of this episode

  1. Current (October 26, 2026): redrawn arrows and three other drawing fixes, same narration · shown above
  2. Original (October 26, 2026) · Watch the previous version (Unlisted on YouTube)

Chapters

  1. 0:00The question
  2. 1:03The claim
  3. 2:48How the proof goes
  4. 4:50Where it stands

The claim, in plain words

A 3-SAT formula is a list of rules about on-off switches. Each rule, called a clause, names up to three switches and asks that at least one of them be set a certain way. Our small example has four switches and four clauses, and of the 16 ways to set the switches, nine satisfy every clause, as our computer checks. Each extra switch doubles the number of settings, so trying them all takes about 2^n steps for n switches.

Cleverer algorithms, as the paper recounts, are still exponential. Schöning’s random walk from 1999 takes about (4/3)^n, and the best bounds it cites for 3-SAT are close to 1.3^n. The Exponential Time Hypothesis, which the paper cites to a 2001 paper by Impagliazzo and Paturi, says that 3-SAT needs 2^(δn) time in the worst case, for some fixed positive δ. It and its strong version became standard assumptions, behind lower bounds for problems from finding cliques to comparing strings.

Result 378, added on October 26, is one OpenAI paper, 67 pages, dated October 17 and revised October 25, 2026, titled The Exponential Time Hypothesis is False. It claims that for every fixed clause width k, two or more, a deterministic algorithm counts exactly how many settings satisfy a k-SAT formula with n variables and m clauses. It uses polynomial space, and time polynomial in n plus m, times 2 to the power C·n log log n / √(log n), where the constant depends on k.

Divided by n, that exponent shrinks to zero, slowly, so it eventually drops below every fixed δ. The paper says this refutes the hypothesis, and also its strong, gap, nondeterministic and counting versions. From its sharper bound for sparse formulas, it then derives a circuit lower bound: a language in E^NP that needs more than a constant times n√(log n) gates, for infinitely many input lengths.

What it doesn’t claim

Not claimed: that P equals NP, since the time bound is still far above polynomial; or that every NP problem gets faster, because, as the paper notes, bounds like this do not carry over through general polynomial-time reductions. The constants are not explicit, and the paper makes no claim about practical speed. By our computation, the explicit parameters in its overview only start to work once n has more than three billion digits; smaller inputs fall back to exhaustive search. And the circuit bound is not a superpolynomial lower bound for NP.

Where it stands

Posted as a preprint
OpenAI, 67 pages, dated October 17, revised October 25, 2026; added to the repository October 26
Under expert review
Per OpenAI: an independent working group led by Russell Impagliazzo, Ramamohan Paturi and Ryan Williams “will examine and explain the proof”
Peer reviewed
Not yet
Formalized in Lean
A weaker bound, exponent n(log log n)²/√log n (scope, comparator); not run by us

Last checked October 26, 2026. On expert review, OpenAI’s release notes say: “An independent working group of computer scientists led by Russell Impagliazzo, Ramamohan Paturi, and Ryan Williams will examine and explain the proof. At the group’s request, we are making the materials public immediately so others can examine them as well.” The paper is not peer reviewed, and we found no public expert assessment yet. OpenAI’s Lean proof (not run by us) covers the paper’s weaker bound with log log n squared in the exponent, still subexponential time in polynomial space; the sharper bounds of its Theorem 1.1, the fixed-density case and the circuit lower bound are not formalized. By our count the Lean development takes 3,091 files and 547,460 lines, excluding Mathlib, much of it a verified machine implementation. OSVerify has not reviewed it.

How the proof goes

  1. An exact formula, and groups that multiply. The proof starts from an exact formula. Each clause becomes a polynomial that is one when the clause is satisfied and zero when it is not, and the count is the sum, over all settings, of the product of these polynomials. If the variables split into groups that no clause crosses, the count is just the product of the group counts: our 12-variable example needs 48 settings instead of 4,096. Real formulas do not split like that. So the paper’s overview first reduces to formulas in which every variable appears at most three times, using sparsification, then Tovey’s copying trick; our computer confirms that the copying steps keep the count.
  2. Bend, split, and come back. Then it bends the formula. Inside every clause, each variable is replaced by a linear form whose coefficients are polynomials in a new parameter T. At T equals zero nothing changes, so the bent sum at zero is still the count. At the points one up to Q, each clause reads only its assigned group plus a few shared integer measurements, and fixing those measurements splits the sum into a product of group sums again. The algorithm computes enough Taylor coefficients at each point and interpolates back to zero, as in our small check.
  3. Low degree from a binomial window. This only pays off if the forms have low degree, and the new construction provides that: a matrix built from commuting swap permutations and a polynomial that matches plus or minus one on a short window of a binomial distribution. The few directions outside the window become the shared measurements; our computer verifies the construction at toy size. Balancing groups, measurements and Taylor data makes all three costs subexponential. The main text then replaces clauses by short parity tests built from expander codes and uses polynomials of Beigel and Tarui, which gives a slightly weaker bound. For the sharper stated bound, an appendix swaps the core step for a different method and finishes with tensor contraction.

The numbers in the video

  • Ours: our 4-variable, 4-clause formula has 9 satisfying settings of 16, by brute force and by the sum of products of clause polynomials.
  • Ours: a 12-variable formula made of 3 groups that never mix has 648 = 9·9·8 solutions, found from 48 local settings instead of 4,096.
  • Ours: OR gates and Tovey cycles keep the count in 4 random trials; a degree-30 polynomial is recovered from 4 Taylor coefficients at each of 8 points.
  • Ours: the paper’s matrix M₀ = V₀ f(W₀) built at toy size (1,024 coordinates) fixes 918 basis directions; the other 106 are measured, and rank(I − M₀) = 106.
  • Ours: the explicit parameters in the paper’s overview pass their own checks only once n has more than 3.28 billion digits; the chart of the exponent divided by n sets the unknown constant to 1 and shows its shape only.

Read the source

The paper

OpenAI groups related papers into one result; this one has a single paper.

Transcript

Read the full script

0:00The question

A 3-SAT formula is a list of rules about on-off switches. Each rule, called a clause, names up to three switches and asks that at least one of them be set a certain way. Our small example has four switches and four clauses, and of the 16 ways to set the switches, nine satisfy every clause, as our computer checks. Each extra switch doubles the number of settings, so trying them all takes about 2^n steps for n switches. Cleverer algorithms, as the paper recounts, are still exponential. Schöning’s random walk from 1999 takes about (4/3)^n, and the best bounds it cites for 3-SAT are close to 1.3^n. The Exponential Time Hypothesis, which the paper cites to a 2001 paper by Impagliazzo and Paturi, says that 3-SAT needs 2^(δn) time in the worst case, for some fixed positive δ. It and its strong version became standard assumptions, behind lower bounds for problems from finding cliques to comparing strings.

1:03The claim

Result 378, added on October 26, is one OpenAI paper, 67 pages, dated October 17 and revised October 25, 2026, titled The Exponential Time Hypothesis is False. It claims that for every fixed clause width k, two or more, a deterministic algorithm counts exactly how many settings satisfy a k-SAT formula with n variables and m clauses. It uses polynomial space, and time polynomial in n plus m, times 2 to the power C·n log log n / √(log n), where the constant depends on k. Divided by n, that exponent shrinks to zero, slowly, so it eventually drops below every fixed δ. The paper says this refutes the hypothesis, and also its strong, gap, nondeterministic and counting versions. From its sharper bound for sparse formulas, it then derives a circuit lower bound: a language in E^NP that needs more than a constant times n√(log n) gates, for infinitely many input lengths. Not claimed: that P equals NP, since the time bound is still far above polynomial; or that every NP problem gets faster, because, as the paper notes, bounds like this do not carry over through general polynomial-time reductions. The constants are not explicit, and the paper makes no claim about practical speed. By our computation, the explicit parameters in its overview only start to work once n has more than three billion digits; smaller inputs fall back to exhaustive search. And the circuit bound is not a superpolynomial lower bound for NP.

2:48How the proof goes

The proof starts from an exact formula. Each clause becomes a polynomial that is one when the clause is satisfied and zero when it is not, and the count is the sum, over all settings, of the product of these polynomials. If the variables split into groups that no clause crosses, the count is just the product of the group counts: our 12-variable example needs 48 settings instead of 4,096. Real formulas do not split like that. So the paper’s overview first reduces to formulas in which every variable appears at most three times, using sparsification, then Tovey’s copying trick; our computer confirms that the copying steps keep the count. Then it bends the formula. Inside every clause, each variable is replaced by a linear form whose coefficients are polynomials in a new parameter T. At T equals zero nothing changes, so the bent sum at zero is still the count. At the points one up to Q, each clause reads only its assigned group plus a few shared integer measurements, and fixing those measurements splits the sum into a product of group sums again. The algorithm computes enough Taylor coefficients at each point and interpolates back to zero, as in our small check. This only pays off if the forms have low degree, and the new construction provides that: a matrix built from commuting swap permutations and a polynomial that matches plus or minus one on a short window of a binomial distribution. The few directions outside the window become the shared measurements; our computer verifies the construction at toy size. Balancing groups, measurements and Taylor data makes all three costs subexponential. The main text then replaces clauses by short parity tests built from expander codes and uses polynomials of Beigel and Tarui, which gives a slightly weaker bound. For the sharper stated bound, an appendix swaps the core step for a different method and finishes with tensor contraction.

4:50Where it stands

The paper is a preprint, not peer reviewed. On expert review, OpenAI’s release notes say that an independent working group of computer scientists, led by Russell Impagliazzo, Ramamohan Paturi and Ryan Williams, will examine and explain the proof, and that at the group’s request the materials were made public immediately, so others can examine them as well. OpenAI also published a Lean proof, not run by us, of a slightly weaker bound, with (log log n)² in the exponent; that is still subexponential time, in polynomial space. If it holds, the Exponential Time Hypothesis is false, and the lower bounds that rest on it or on its strong version lose that basis, though some also follow from weaker hypotheses that may still hold.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.