Complexity theorists to examine OpenAI's claimed Exponential Time Hypothesis refutation

OpenAI says an internal model has refuted the Exponential Time Hypothesis (ETH), and on Monday three complexity theorists announced they will lead an open, independent examination of that claim. Two of them, Russell Impagliazzo and Ramamohan Paturi of UC San Diego, proposed ETH in the first place, together with Francis Zane. The third is Ryan Williams of MIT.

Williams put it plainly on X: "An internal model at OpenAI has produced a claimed refutation of ETH! Russell Impagliazzo, Mohan Paturi, and I have been asked to help organize an open and independent examination of this claim."

This is the part of OpenAI's three-discovery announcement that I find most interesting, and not because of the claim. It is because of the procedure.

What ETH is, and why anyone cares

The conjecture concerns how hard it is to solve Boolean satisfiability, a problem closely tied to P versus NP, according to The Next Web. Researchers have used it to argue that problems in graph theory, computational biology, databases and other fields cannot be solved quickly. Hundreds of computer science papers rest on it, TNW reports.

So a refutation, if it holds, does not knock down one result. It knocks on the foundation of a lot of hardness arguments. The three researchers say as much: "If the claim is correct, it will change an important part of theoretical computer science."

That sentence has an "if" in it, and the authors meant it. In an open letter, Impagliazzo, Paturi and Williams wrote: "Our involvement should not be taken as certification of the claim. A result of this significance requires careful, independent scrutiny." Read that twice. The people running the check are telling you in advance that a check is not an endorsement.

The timeline and the artifacts

According to OpenAI, its model found the disproof on October 16. The company verified it in Lean, a language that checks proofs by machine, the next day, and has published the model's write-up and the Lean proof on GitHub. That is a good sign in the way a lab notebook is a good sign: it gives other people something to run.

What the announcement does not include is any account of the model itself. The architecture, training method and workflow behind the refutation are not described. The cited reports do not establish whether an outside party has compiled the Lean proof. Those are the first two questions I would put to anyone claiming a result like this, and they are still open.

OpenAI's blog post, titled "Working with academic communities to build scientific understanding," describes its approach this way: "In our view, these manuscripts are best understood as a form of raw research data." The company says it asked outside experts to act as shepherds and organize groups to understand the results. For the computer science result, the stated plan is to form an external group to explain the result while making the AI output public "for anyone to examine and build on."

The terms, as reported:

• No nondisclosure agreements. Participants can discuss the work, share intermediate products and publish their conclusions.
• OpenAI says it does not seek academic credit for discoveries produced by its internal models.
• The three theorists will not be paid, according to Williams.
• They asked OpenAI to release all raw data on the ETH result and to fund a conference for the research community. OpenAI agreed to both, per Williams and OpenAI.

OpenAI has also given $5 million to the Simons Foundation for workshops and conferences on AI-produced results, TNW reports.

Not every result gets the same treatment

The ETH material is public. The physics material is being held back for now. Nobel laureate David Gross will lead that group, with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov. According to TNW, the group chose not to release the AI-produced material for now and will write up the work itself.

That result is the larger claim: OpenAI says its models produced a rigorous proof that certain quantum field theories exist in four dimensions, including quantum chromodynamics and pure Yang-Mills theory, which is part of a Clay Mathematics Institute Millennium Prize problem. In mathematics, OpenAI says its models proved Christopher Sogge's 1991 local smoothing conjecture in every dimension, which would also settle the Kakeya and Stein restriction conjectures. Mathematicians had proved local smoothing in two dimensions in 2019 and Kakeya in three dimensions in 2025.

Golden Era reported that the initial announcement posts omitted researcher names and verification details. TNW's account names the academic leads and reports that Lean proofs and write-ups for the math and computer science results were published on GitHub.

What to watch

The cited reports give no timetable for the examination group's conclusions. Watch for three things:

1. Whether independent people compile the Lean proof, and what they find about the formal statement being proved versus the statement ETH actually makes.
2. When Impagliazzo, Paturi and Williams publish conclusions, and whether they read like a verdict or a progress report.
3. When the Gross group releases its write-up or the underlying material, and whether the Clay Mathematics Institute says anything about pure Yang-Mills.

There is also the credit question the three researchers raised: how it should be assigned when AI finds a result first. Mathematicians raised similar concerns in the Leiden declaration in June.

My view: the most credible thing OpenAI has done here is invite independent scrutiny, including from two of the people who proposed the hypothesis. A press release is a claim. A Lean file, a public write-up and three skeptics with no NDAs are an experiment.