OpenAI says its model refuted ETH: how you actually check a machine discovery

On October 26 OpenAI announced that an unnamed internal model had disproved the Exponential Time Hypothesis, the conjecture that 3-SAT cannot be solved in subexponential time and the assumption behind hundreds of conditional hardness results. In the same post it claimed a proof of Sogge's 1991 local smoothing conjecture in every spatial dimension, which OpenAI says also settles the Kakeya and Stein restriction conjectures, plus rigorous existence proofs for interacting four-dimensional quantum field theories including QCD. Any one of these would be the result of a career. Nobody outside OpenAI has confirmed any of them yet. The interesting question for an engineer is how you would go about checking.

What was actually released

According to Interesting Engineering's report, the ETH disproof was produced on October 16 and formalized in Lean the next day. The local smoothing proof followed on October 18, also with a Lean formalization a day later. The physics work has no public artifacts at all: a group led by David Gross, with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov, will write its own explanation before the model output is released. The ETH claim goes to Russell Impagliazzo and Ramamohan Paturi of UC San Diego and Ryan Williams of MIT, and OpenAI has agreed to fund a conference on it.

The artifacts live in the public openai/math repository. Its README is more candid than the press cycle. It describes 721 manuscripts in 373 families, says roughly 42% of top-line results are formalized, calls the manuscripts "raw research data" rather than polished papers, and states plainly that "some of the unformalized results could have issues." Most results came from one procedure: about 4,000 posed problems, averaging around three hours of ChatGPT Pro thinking compute per result. That is a search process with a filter at the end, and the strength of the filter is what decides how much of the output survives contact with experts.

A Lean proof checks one statement, not the press release

The ETH case is the cleanest test because it comes with a formal artifact. The scope note for the formalization says Lean proves that, for each fixed clause width k of at least 2, a deterministic machine exactly counts the satisfying assignments of a canonically encoded k-CNF formula. The time bound is polynomial in the input length times 2 raised to n (log log n) squared over the square root of log n, with constants depending on k, and the machine touches only polynomially many tape cells. That exponent grows slower than any linear function of n, which is what subexponential means, and counting is at least as hard as deciding. If the definitions are right, ETH falls, and the Strong ETH goes with it because it implies ETH.

A green Lean build tells you the proof matches the statement. It tells you nothing about whether the statement matches the claim.

The note also shows the gap. The sharper bounds in the October 25 manuscript, one in terms of the clause count m and a better one for formulas with m at most a constant times n, are attributed to the manuscript, not to the Lean proof. AiCybr's walkthrough points out the comparator challenge file states the target theorem with a sorry placeholder, which is correct practice: a separately written statement that the proof must match. It also notes that no runnable SAT solver ships with the claim. I covered the same trap in the piece on what formal proofs exclude: the trusted base is the theorem statement plus every definition it depends on.

My verification order

For the ETH result, I would start with the definitions, not the proof. How is the machine model defined, what does "canonically encoded" mean, and does the time bound count the steps that matter? A subtle cheat in the cost model, such as a primitive that does exponential work in one step, would let a correct proof prove a meaningless theorem. Second, I would run the Lean axiom printout on the main theorem and confirm it relies only on the standard axioms with no extra declarations hiding a gap. Third, I would build the whole library from a pinned toolchain on a clean machine, because a proof that only compiles on the author's cache is not a proof. Only then does reading the manuscript make sense.

For local smoothing, the question is scope. OpenAI's own framing says all dimensions; press coverage quoting the manuscript describes the Kakeya and restriction consequences more narrowly. Check exactly which statement Lean proves and which ranges of exponents it covers. For the QCD and Yang-Mills claims, there is nothing to check yet. No artifacts, no formalization mentioned in the coverage, and a field where the definition of "existence" is itself the hard part. Until the Gross group publishes, that claim has zero evidential weight, however impressive the names.

The limitation I cannot get around: none of this checks novelty. The repository says it defers to the community "on matters of credit, precedence, and concurrent work," and a Lean proof cannot tell you whether a human published the same argument in 2009. That part still needs people who know the literature, which is why I think verification is the new bottleneck more than generation.

The takeaway for your own pipelines

If you use models to produce anything that claims to be correct, whether proofs, refactors or migration scripts, copy the structure OpenAI used for ETH, not the announcement. Write the target statement separately from the generator, have it reviewed by someone who did not see the output, and make the checker the only path to "done." Then treat everything that did not pass through the checker the way OpenAI's own README does: as raw data that could have issues.