An AI says it broke a 27-year-old hypothesis. Who checks?

On 26 October 2026, OpenAI said its AI system had proved the Exponential Time Hypothesis false. The hypothesis dates from 1999. Hundreds of papers assume it. OpenAI says the proof was checked in Lean, a proof assistant, one day after the AI wrote it.

Nobody outside OpenAI has confirmed it. Russell Impagliazzo, Ramamohan Paturi and Ryan Williams are reviewing it, and Impagliazzo and Paturi proposed the hypothesis. This post is about why a computer-checked proof still needs them. Lean proves exactly the statement it is given. Someone has to check that the statement is the famous problem.

Maths. In 1991 Christopher Sogge proposed the local smoothing conjecture. Roughly, it says a wave can focus sharply at its worst moment, and much less at a typical one. Guth, Wang and Zhang proved it in two dimensions in 2019. OpenAI says its models proved it in every dimension. Local smoothing implies the Kakeya conjecture and Stein’s restriction conjecture, so OpenAI says those are settled in all dimensions too. The AI output is dated 18 October and the Lean proof 19 October. Both are public on GitHub.

Computer science. OpenAI says its system found a disproof of the Exponential Time Hypothesis (ETH) on 16 October and formalised it in Lean on 17 October. The writeup and the Lean files are public. Impagliazzo and Paturi of UC San Diego and Williams of MIT are verifying it.

Physics. OpenAI says its models proved that certain four-dimensional quantum field theories exist as rigorous mathematical objects, among them quantum chromodynamics (QCD). The work builds on Balaban’s constructive approach. It includes the existence of pure Yang–Mills theory, which is one part of a Clay Millennium Prize problem. The other part, the mass gap, is not claimed (MindStudio), so the prize is not in play. The proofs are dated 9 and 18 September. OpenAI says it waited for the Lean formalisation of Yang–Mills existence, which finished on 16 October. None of it is public. David Gross, Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov decide when it is released.

Each result is being released a different way: maths in the open, CS through Impagliazzo, Paturi and Williams with everything public, physics held back by Gross, Douglas, Jaffe, Klebanov and Nekrasov. OpenAI writes, “We do not yet know which of these three approaches will be most useful.”

A k-CNF formula is an AND of clauses. Each clause is an OR of at most k variables or their negations. Satisfiability asks whether some setting of the variables to true and false makes the whole formula true. Trying every setting of n variables takes 2ⁿ steps. The best known algorithms for 3-SAT do better, at about 1.3ⁿ. That is still exponential.

ETH, proposed by Impagliazzo and Paturi in 1999, says it has to be. There is some constant c > 1 such that no algorithm solves 3-SAT in fewer than cⁿ steps. An algorithm that beats every such c is called subexponential.

ETH became a standard assumption. A researcher shows that a fast algorithm for some problem would break ETH, and concludes the problem is hard. OpenAI says hundreds of papers do this, in graph theory, computational biology, databases and computational geometry. If ETH is false, those proofs stay correct. Their conclusions lose the assumption they rest on.

OpenAI’s claim goes further than a fast SAT algorithm. The Lean documentation says that for fixed k ≥ 2, a deterministic machine exactly counts the satisfying assignments of a canonically encoded k-CNF formula in subexponential time and polynomial space. Counting is at least as hard as deciding: a count above zero means the formula is satisfiable. So the counting result, if it holds, refutes ETH.

Williams told Al Jazeera that he, Impagliazzo and Paturi are “working to verify and examine their proof and determine if it holds up.” He also said it would have no real-world use in the short term.

Lean is a proof assistant. You write definitions and a theorem in its language, then a proof. A small program inside Lean, the kernel, checks every step. If the kernel accepts, the proof is correct for the statement as written. It does not matter who wrote the proof, a person or an AI.

OpenAI publishes its Lean work for Comparator, a checker from the Lean project. Each result comes in two parts. A challenge file states the theorem and every definition it uses, with sorry where the proof would go. That is Lean’s word for “not proved yet.” A separate solution module holds the proof. Comparator confirms three things: the solution proves the same statement as the challenge, it uses no axioms beyond an allowed list, and the kernel accepts it.

For the maths and CS results, OpenAI says that took one day from the AI’s output. The physics formalisation took about five weeks and has not been published. Then the people came in: an unnamed expert for maths; Impagliazzo, Paturi and Williams for CS; Gross, Douglas, Jaffe, Klebanov and Nekrasov for physics.

Lean checks the proof against the statement. It cannot check the statement against the problem as complexity theorists understand it. Here is the theorem in OpenAI’s ETH challenge file, with some bookkeeping cut:

A reviewer has to ask three questions of it.

1. Do the definitions match the original problem?

Every term in the theorem is defined in the same file, in about 200 lines. A reviewer reads each one against the textbook definition.

The input. encodeCNF writes n in unary, then each clause as a sorted list of literal codes. This is what “canonically encoded” means. The time bound may grow with a power of L, the length of that encoding. A clause has at most k literals and no clause repeats, so L is at most polynomial in n. That factor cannot hide exponential work. A reviewer has to redo that reasoning, not take it on trust.

The machine. PrimitiveMachine is a multi-tape Turing machine over bits, built on Mathlib’s Turing-machine library. Its transition is a function, so it is deterministic. Time is the number of steps in a trace. Space is the number of tape cells visited, across all tapes.

“Subexponential”. The bound is 2 raised to a constant times this:

That is n · (log log n)² / √(log n), with n shifted by 16 to keep the logarithms positive. It grows more slowly than any constant times n, so the bound is subexponential in the sense ETH needs. The 25 October manuscript claims a sharper bound, with log log n in place of its square. The Lean file proves the weaker one. So the paper has to be checked against the Lean as well.

The order of the quantifiers. The theorem says there is one machine, and then that it works for every n and every formula. Flip the order, to “for every n there is a machine,” and a lookup table for each n would satisfy it. The theorem would then say nothing. The order here is right. It comes down to where one symbol sits, and a person has to look.

2. Are there extra assumptions in the axioms?

A Lean proof can declare an axiom, a statement accepted without proof. One false axiom proves anything.OpenAI’s Comparator settings allow three: propext, Quot.sound and Classical.choice. These are the standard axioms Mathlib is built on. Comparator rejects a proof that uses any other. The challenge file imports only Mathlib, so a reviewer also trusts Mathlib’s definitions, which is the usual bargain. The ETH settings leave off an optional second kernel, nanoda, that would recheck the proof independently.

3. Is any step left unfinished?

The challenge file ends in sorry on purpose, because it is the question. A sorry left in the solution would show up as an axiom called sorryAx. That is not on the allowed list, so Comparator would fail. This check is mechanical. It only counts once someone outside OpenAI runs it. None of the reports we read say anyone outside OpenAI has done so yet.

So a program anyone can run settles two of the three questions. The first is the one that needs Impagliazzo, Paturi and Williams. The maths result has the same gap. Its local smoothing theorem is stated for Schwartz functions, through a half-wave operator and an “observation measure” defined in the same file. An analyst has to confirm those match Sogge’s conjecture. For physics, nobody outside can ask any of the three questions yet.

A proof also has a layer Lean never sees: the writeup’s references. We ran hedwigai’s reference check on the public writeup, Local smoothing for the Euclidean wave equation (25 October 2026). We gave it the 84 sentences that cite a work, word for word, and all 81 references. Every reference is cited, and the text cites nothing the list lacks.

So every reference in the writeup exists, and none is retracted. Our checker flagged 25 that were fine, and we cleared each one by hand. That is this post’s point at a smaller scale. A tool checks what it can reach, and a person checks the tool. We then fixed the checker. Run again on 30 October, it flagged 6: OpenAI’s three preprints, a book and a 1980 paper our sources did not find, and a book Crossref itself dates to 2001.

Then the harder question: does each work say what the sentence citing it claims? The check reads each cited paper’s open copy, and where the paper is on arXiv, its LaTeX source, so a sentence citing “Corollary 1.3” is read against Corollary 1.3. It read the 84 sentences as 85 claims.

Seven citations hold where the check could see the cited result, and none was contradicted. The other 77 are not shown wrong. For them the check found no passage that says what the sentence says, in its words. Gao et al. show how that happens: their Corollary 1.3 is a formula in n and p, and the 2/9 the sentence cites appears only in a table of its cases. Those citations still need an analyst with the paper open.

First, Impagliazzo, Paturi and Williams. OpenAI has agreed to their requests to make all raw data public and to fund a conference on what the result means. Second, the physics release, which Gross, Douglas, Jaffe, Klebanov and Nekrasov decide. Third, whether anyone outside OpenAI runs Comparator on the public results and reports what they found.

The same rule applies to an ordinary paper. A tool checks what you give it. If you write with AI help, check that every reference exists and says what you cite it for.