OpenAI publishes the prompt behind its ETH refutation claim

OpenAI has released the prompt behind its claim that the Exponential Time Hypothesis (ETH) is false, and the prompt set a smaller target than that claim. It asked a model to refute the deterministic Strong Exponential Time Hypothesis (SETH) by finding one fixed saving over brute-force search that works for every clause width k >= 3. The text, published by Ethdiscussion on November 13 after OpenAI agreed to make it public, tells you how the task was set. It says nothing about whether the proof holds. That question sits with a group led by Russell Impagliazzo, Ramamohan Paturi and Ryan Williams, which OpenAI said will verify the claim.

The difference between the two hypotheses explains why the target was smaller. ETH says 3-SAT needs exponential time: there is some δ > 0 for which no algorithm solves it in O(2^δn). SETH goes further and says the best exponent for k-SAT climbs toward brute force’s 2^n as k grows, which Impagliazzo and Paturi write as lim s_k = 1. The prompt only asked for a proof that this limit is below 1. If ETH really is false, k-SAT for each fixed k runs in less than any exponential, and that refutes SETH with room to spare. OpenAI’s manuscript, titled “The Exponential Time Hypothesis is False,” claims that larger result. It sits in the company’s openai/math repository on GitHub.

Most of the prompt is about closing loopholes. The model had to prove that its algorithm terminates and is correct on every input, whether satisfiable or unsatisfiable. It had to show a lower bound on epsilon that doesn’t depend on k. And it had to account for every cost: input reading, sparsification, subroutine calls and any derandomization. The prompt also spelled out what wouldn’t count: savings that shrink to zero as k grows, gains for only finitely many widths, average-case or promised-input algorithms, unsupported oracle steps, and randomized algorithms with no valid deterministic conversion. It warns that a paper by Cygan et al. uses bounded-error randomized algorithms and that this convention should be kept separate. A conditional result was not to be labeled unconditional. If no refutation came out, the model was to say so plainly. “Useful rigorous partial progress is preferable to a fabricated solution,” the prompt says.

The model found the argument on October 16, and the Lean proof assistant checked it the next day. Human review, by contrast, is only at its first step. TechCrunch reported that computer scientists formed a working group and asked OpenAI to share the proofs publicly and fund a conference. The group’s first move was an open letter asking for feedback and a discussion of norms for AI contributions. OpenAI asked Williams to help interpret the solution together with Impagliazzo and Paturi, who first published ETH in 1999.

The same TechCrunch report adds two complications. Levent Alpöge, a mathematician at Anthropic, suggested that OpenAI was building its solutions on existing work, and hours later Anthropic released its own refutation of ETH. Williams had earlier called OpenAI’s October proof dump a “DDOS attack on mathematicians” before agreeing to collaborate.