OpenAI says a model disproved a computer-science assumption. The referees have not signed it

OpenAI said on 26 October that an internal system had produced three research results, in computer science, mathematics and physics, and that it was handing them to outside groups rather than treating the blog post as the last word. The one that travels furthest is a claim that the exponential time hypothesis is false. That hypothesis, from the 1990s, says a class of hard logic puzzles cannot be solved much faster than trying the possibilities. A large later literature assumes it. If the claim survives, those papers need a new foundation. OpenAI’s own post says a faster argument on paper is not yet a faster program anyone can run.

The dates in the post are specific. The system produced a natural-language disproof on 16 October, and a formalization in the Lean proof checker the next day. The paper and the Lean file are public. The people asked to examine it are Russell Impagliazzo and Ramamohan Paturi, who posed the hypothesis, and Ryan Williams of MIT. Their willingness to look is not a verdict. On 27 October Anthropic said an internal Claude model had produced its own refutation of the same hypothesis, also on 16 October, also with a Lean proof. Two labs claiming the same landmark on the same day is a reason to read both files. It is not a reason to close the question.

The mathematics claim is a different file. OpenAI says the model produced, on 18 October, a proof of the local smoothing conjecture in every dimension, formalized in Lean the next day, and that this would also settle the Kakeya conjecture and Stein’s restriction conjecture in all dimensions. Kakeya in three dimensions was proved by Wang and Zahl in 2025. The step to every dimension is the new claim, and it is on the same public repository. A formal file can still fail to mean what the English sentence says. That comparison is the check that has not been finished.

The physics claim is the one not on the table. OpenAI says the system wrote an existence argument for pure Yang–Mills on 9 September and for quantum chromodynamics on 18 September, and formalized the Yang–Mills existence proof in Lean on 16 October. Existence of Yang–Mills is one part of a Clay Millennium problem. The prize also asks for a mass gap, which this announcement does not claim to have proved. A group led by David Gross, with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov, is holding the artifacts and will decide how they are released. Until that file is public, the third result is a press post.