AI Just Challenged a Fundamental Limit of Computing. We Put the Maths to the Test.

On 26 October OpenAI added a paper to its public openai/math repository with a blunt title: "The Exponential Time Hypothesis is False". If it holds up, it is one of the bigger results in theoretical computer science for a long time. It also arrived with a lot of noise, so I want to set out what the claim is, what has and has not been checked, and what it means for people who build and run real systems. Short version: it is genuinely interesting, it is not yet confirmed by the wider community, and it does not break anything you rely on today.

I have since tested the idea against my own software. The measured results, including where nothing changed, are in what I found when I tested my own projects.

What the Exponential Time Hypothesis is

Start with 3-SAT. You get a formula made of clauses, each clause is an OR of at most three variables (or their negations), and the whole formula is the AND of all the clauses. The question is whether some true/false assignment of the variables makes every clause true. It is the textbook NP-complete problem.

The obvious algorithm tries every assignment. With n variables that is 2ⁿ possibilities. Cleverer algorithms do better, but every known one still takes time that looks like 2^cn for some constant c below 1.

In 2001 Russell Impagliazzo and Ramamohan Paturi turned that observation into a precise conjecture. The Exponential Time Hypothesis (ETH) says there is some constant c > 0 such that no algorithm solves 3-SAT in time 2^cn. In plain terms: you can shave the exponent, but you cannot get rid of it. 3-SAT needs genuinely exponential time.

That is a stronger statement than P ≠ NP. P ≠ NP only says there is no polynomial algorithm. ETH also rules out everything in the huge gap between polynomial and exponential, such as 2^√n or 2^{n/log n}. Those are called subexponential.

Why computer scientists believed it

Three reasons, roughly.

First, decades of effort. Algorithms such as PPSZ (Paturi, Pudlák, Saks and Zane) and its later refinements pushed the constant c down for 3-SAT, but never to zero. Each improvement was hard won and small. Nobody had a credible route to a subexponential algorithm for general 3-SAT.

Second, the sparsification lemma, also from Impagliazzo, Paturi and Zane. It shows that any k-CNF formula can be split into a manageable number of sparse formulas, where the number of clauses is only linear in the number of variables. That made ETH robust: it does not matter much whether you measure by variables or by clauses, and it lets you reduce from 3-SAT to other problems without losing the exponential.

Third, and most important in practice, a whole field was built on top of it. Hundreds of conditional lower bounds take the form "this problem cannot be solved faster than X unless ETH fails". Graph colouring, clique, many parameterised problems and a lot of fine-grained complexity results lean on ETH or its stronger cousin, SETH. ETH was less a belief than load-bearing infrastructure.

What OpenAI has reported

The openai/math repository on GitHub is released under Apache-2.0. According to its README it holds 721 manuscripts in 373 result families, produced by an unreleased internal model, each using on average about three hours of ChatGPT Pro thinking compute. Roughly 42% of the top-line results come with Lean formalisations.

OpenAI is careful about what this collection is. The README calls the manuscripts "raw research data, rather than polished academic papers" and warns that "Some of the unformalized results could have issues." That framing matters for everything that follows.

The ETH paper went into the repository's history.md on 26 October 2026. The entry reads:

"The paper gives a deterministic algorithm that exactly counts satisfying assignments of fixed-width CNF formulas in subexponential time and polynomial space. The case of 3-SAT refutes the Exponential Time Hypothesis. 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."

Note what is claimed. It is not just deciding satisfiability: it is exactly counting the satisfying assignments (#SAT), deterministically, in polynomial space. Counting is at least as hard as deciding, so if counting is subexponential then 3-SAT is too. And the working group includes Impagliazzo and Paturi, the two people who stated the hypothesis.

What the formal proof covers, and what it does not

This is the part most coverage has blurred. There is a Lean formalisation, documented in lean/docs/378.md, with the checked statement in lean/ComparatorChallenges/SubexponentialSAT.lean. Lean is a proof assistant: if it accepts a proof, the stated theorem follows from the definitions, with no gaps a human reviewer might miss.

The Lean-checked statement says: for any fixed clause width k ≥ 2, there is a deterministic machine that takes a canonically encoded k-CNF formula on n variables with encoding length L, and counts its satisfying assignments in time

(L+1)^O_k(1) · 2^(O_k(n (log log n)² / √(log n)))

while visiting at most (L+1)^O_k(1) tape cells at every step, which is polynomial space.

The manuscript itself claims sharper bounds than the Lean statement:

So the machine-checked version has an extra (log log n)² factor in the exponent compared with the paper's best claim. For refuting ETH that does not matter: n (log log n)² / √(log n) still grows more slowly than any c·n, so the Lean bound alone is subexponential. But it does mean the sharper numbers in the paper are not what Lean checked.

There is a second, more important limit. Lean checks that the proof proves the stated theorem. It does not check that the stated theorem means what we think it means. Encodings, machine models and definitions all have to be read by humans to confirm the formal statement really captures "3-SAT in subexponential time" in the usual sense. That is exactly the kind of thing the working group led by Impagliazzo, Paturi and Williams will be looking at. A Lean-checked bound is strong evidence. It is not the same as the community reading, understanding and accepting the whole manuscript, and as of 27 October the press reports I have seen describe no independent confirmation yet.

Why independent scrutiny matters

This is not me being sceptical for the sake of it. The same repository shows why review is needed.

On 7 October 2026 the repository withdrew three manuscripts after a sign error was found, and revised 14 others. That is not a scandal. That is the process working: material was published openly, someone checked it, problems were found, and the record was corrected in public. It is exactly why OpenAI calls the collection raw research data, and exactly why a working group is reading this paper before anyone declares the matter closed.

For a result this significant, the bar is high and should be. I would expect weeks to months of careful reading, talks, simplified write-ups and probably some fixes before the field treats it as settled. If it survives that, it is historic. If it does not, the open process will have shown where it failed.

What subexponential actually means

"Subexponential" sounds like "fast". It is not. Here is the paper's headline shape, 2^{n/√(log₂ n)}, compared with brute force 2ⁿ and a polynomial, n³. These ignore every hidden constant, which I will come back to.

For n = 100, log₂ n is 6.64, its square root is 2.58, so the exponent drops from 100 to 38.8. That is a huge relative saving, and it gets bigger as n grows. But look at the last column. By n = 1,000 the subexponential figure is already around 10⁹⁵, far beyond anything any computer will ever do, while n³ is a billion.

The reason is that √(log n) grows extremely slowly. 2^{n/√(log n)} still grows faster than n^c for any fixed c. It is not polynomial and it is nowhere near it. The small-n row where it beats n³ is an artefact of ignoring constants.

And the constants are not small. The O_k(·) notation hides factors that depend on the clause width k and can be enormous, plus a polynomial factor in front. Asymptotic results like this tell you the shape of the curve as n heads to infinity. They tell you nothing about whether the algorithm wins at the sizes you actually run.

Why this does not imply P = NP

P = NP would need a polynomial algorithm for 3-SAT, something like n³ or n¹⁰⁰. This result, if correct, gives 2^{n/√(log n)}-ish time, which is superpolynomial. It moves 3-SAT out of "genuinely exponential" into the grey zone between exponential and polynomial. It says nothing about whether the polynomial end is reachable.

What it does do is knock out ETH as an assumption. Any lower bound of the form "unless ETH fails" loses its foundation and needs either a new assumption or a fresh look. That is a big deal for theorists. It is not P = NP.

Why modern encryption is not automatically broken

I have already seen the "AI breaks encryption" headlines. They are wrong, for three separate reasons.

• Different problems. AES, RSA, elliptic curve cryptography and lattice-based schemes do not get their security from fixed-width CNF counting. You can encode any of them as a SAT instance, but the encodings are huge and gain nothing from a bound that is barely subexponential in the number of variables.
• Still superpolynomial. Even on its own problem, the bound grows faster than any polynomial. Key sizes are chosen so that the best known attacks are out of reach by enormous margins.
• Practical attacks need concrete numbers. Cryptanalysis is about actual operation counts for actual key sizes. An asymptotic bound with unknown, k-dependent constants does not tell you how many operations an attack takes on a 256-bit key. Nobody has shown this result gives any concrete speed-up against any deployed scheme.

Keep patching, keep using current TLS settings, keep planning for post-quantum migration. None of that changes this week.

Which ideas are interesting for engineers

I have not reproduced the paper, and I will not pretend to explain its proof in detail. What I can say from the published materials is that it works by exact counting over algebraic, tensor-network style representations of the formula, rather than by searching for a single satisfying assignment.

That family of ideas is not new, and parts of it are already practical:

• Counting rather than searching. #SAT counters built on DPLL-style search with caching and component decomposition already count solutions to large real-world formulas.
• Tensor network contraction. A CNF formula can be written as a network of small tensors; contracting it counts the solutions. The cost depends heavily on the order you contract in, which is a graph problem in its own right and closely tied to treewidth.
• Structure in sparse constraint systems. Real problems are rarely random. Sparse, locally structured constraints can often be split, decomposed or contracted far more cheaply than the worst case suggests.

The established tools to look at are CDCL SAT solvers such as those in the annual SAT competitions, DPLL-based model counters, tensor network contraction libraries, and Google's OR-Tools CP-SAT for scheduling and constraint problems.

What practical engineers can use today

Honestly: the tools above, not this paper. Modern CDCL solvers routinely handle industrial instances with millions of variables because real inputs have structure that worst-case analysis ignores. Nothing derived from this result is going to beat them on real inputs any time soon, and the paper does not claim it will.

The win is conceptual. A hypothesis many of us treated as a fact may not be one. That is a useful reminder to check whether a problem in your own stack is really as hard as everyone assumes, and whether you are reaching for a heuristic when a proper solver would do better.

What I found when I tested my own projects

Status: first results, 27 October 2026. I will add to this section if anything changes.

I audited my own software for anything that is genuinely SAT or #SAT shaped: the ACE WordPress plugins, the AceHost hosting platform, the Fuse Quest game engine, Sheff.Events, a sports news client's site and an industrial client's WooCommerce catalogue. The honest answer is that nothing in any of them is a satisfiability or model-counting problem, and no part of OpenAI's result transfers to them. The only thing that even rhymes with the paper's trick of factorising a huge sum is a fantasy scoring routine, and that is trivial at the sizes people actually use.

So I picked three places where the shape of the work, rather than the theory, looked worth measuring, and benchmarked each one in isolation on a Raspberry Pi 5, with the production code copied unchanged as the baseline and the output checked for equality before timing. The tables show medians.

Redis cache flush and page invalidation

My Redis cache plugin flushes a namespace by scanning for keys and deleting them one at a time, and invalidates a page with 40 separate deletes. Batching the same work into pipelined UNLINK commands removes the round trips.

A generation counter, where a flush is a single increment and old keys simply stop being read, took about 0.05 ms at every size. It is not free: every old key stays in memory until its expiry fires, so every write must carry a TTL. These runs were over loopback, so on a networked Redis the gap is wider. This is plain engineering, not complexity theory.

Fuse Quest: unreachable goals and line of sight

When a character in my game asks for a route to somewhere it cannot reach, A* searches up to its 4,500-node limit before giving up. Labelling the map's connected regions once, then refusing a route in constant time when the start and goal sit in different regions, removes that wasted search. Each row is 400 queries on the real 300 by 300 town map.

Reachable routes come out identical and the difference there is noise. Labelling costs about 16 ms, so it runs when the map changes, not per query. I also checked the 24-sample line of sight test against an exact grid walk over 10,000 random rays per length: at length 8 it missed 53 of 3,158 walls, at length 64 it missed 1,791 of 9,237, and at length 128 it missed 2,649 of 9,879. The test grid uses thin random walls, which exaggerates the gap compared with real buildings, and the exact walk is slower on long rays.

GlossPress glossary highlighting

GlossPress highlights glossary terms by running one regular expression per term over every text node. The textbook fix is Aho-Corasick, which finds every term in one pass. The practical fix turned out to be much smaller: a plain substring check first, running the original regex only when the term is actually present.

The prefilter is about 25 lines, gives byte-identical output and never loses meaningfully. Aho-Corasick only pays off at 1,000 or more terms on long posts, is slower than the original below 100 terms and needs 6 to 25 MB of memory. Real glossaries are tens to low hundreds of terms, and the output cache hides the cost on warm pages anyway. One separate finding: with PHP's default PCRE JIT on, the original code segfaulted reproducibly at 5,000 terms on posts of 20 KB or more on the Pi (PHP 8.4.25 on ARM), because that many patterns overflow PHP's regex cache. Turning the JIT off avoided it. I have not reproduced it on x86 servers, and no real glossary is that large.

What the audit actually found

The useful findings were ordinary ones, the kind any careful review turns up: N+1 database queries inside loops, locks that check and then set in two steps instead of atomically, timezone and midnight boundary bugs in date handling, SQL that wraps an indexed column in a function so the index cannot be used, and cache entries that all expire at the same moment and stampede the database together. None of them needs a new algorithm. All of them are worth more than the exotic ideas above.

Try it yourself: the ACE Complexity Lab

I built the ACE Complexity Lab so you can see these ideas rather than take my word for them. It runs entirely in your browser.

• Exponential growth: compares 2ⁿ, the paper's subexponential shape and a polynomial as you change n, so you can see where each curve actually becomes a problem.
• A real 3-SAT solver: write or generate formulas, including the pigeonhole family and random formulas either side of the 4.26 threshold, solve them in a background worker and count every solution exactly for small ones.
• The DPLL search tree: draws how a backtracking solver splits, propagates and prunes, which is what practical SAT solvers build on.
• Polynomial counting in miniature: walks through the paper's construction in plain words, then runs a small working version (bent linear forms, measurement enumeration and interpolation) that recovers the exact number of satisfying assignments.
• Measurements: the three experiments above as charts and tables, with the trade-offs and verdict for each.

What remains theoretical

• Whether the full manuscript, not only the Lean statement, is correct.
• Whether the sharper manuscript bounds hold, or only the weaker Lean bound.
• Whether the formal statement captures 3-SAT in exactly the standard sense; the working group's reading will settle that.
• How large the hidden constants are, and whether the algorithm can ever be practical at any useful size.
• What happens to the Strong Exponential Time Hypothesis, which is a different and stronger claim.

What future research might unlock

If the result stands, the immediate work is repair: going through the many results conditioned on ETH and finding which survive under weaker or different assumptions. Expect a wave of papers doing exactly that.

Beyond that, a new algorithmic technique that cracks a 25-year-old barrier rarely stays in one place. The same ideas may tighten bounds for other counting problems, improve exact algorithms for graph problems, or feed into better contraction orderings for practical tensor network tools. The same catalogue already contains other claimed results in neighbouring areas:

• Result 130: an exact discrete Fourier transform in O(n (log n)^1−δ) with δ = 10⁻¹³. Asymptotically better than O(n log n), but unusable in practice because the saving only appears at absurd sizes.
• Result 128: a deterministic polynomial-time factor-two approximation for shortest common superstring, explicitly not the classical greedy algorithm.
• Results 113 to 115: FPRAS (randomised approximation schemes) for counting perfect matchings, common matroid bases and contingency tables.
• Result 112: a depth-three circuit lower bound of 2^ω(√n).

Each of those needs the same scrutiny. Taken together, they suggest AI-generated mathematics is becoming a real source of research leads, provided we keep checking the work as carefully as we would anyone else's.

Sources

• openai/math on GitHub (README and CONTENTS.md)
• history.md, entry for 26 October 2026
• lean/docs/378.md and lean/ComparatorChallenges/SubexponentialSAT.lean
• The Exponential Time Hypothesis is False (paper.pdf)
• Exponential time hypothesis, Wikipedia
• Russell Impagliazzo and Ramamohan Paturi, "On the Complexity of k-SAT", Journal of Computer and System Sciences 62(2), 2001