"Proved by AI" in three fields
OpenAI on Oct. 26 (Oct. 27 Japan time) unveiled three research results produced by its AI models. The results concern open problems in mathematics, computer science and physics, and the company said it released the materials in a form that researchers can verify and build on. The company's researcher X account @danintheory and others announced them.
The company has not disclosed which model it used. OpenAI also announced in September a proof of a "blowup solution" to the Navier-Stokes equations, which describe fluids.
| Field | Claim | How it is checked |
|---|---|---|
| Mathematics (harmonic analysis) | Proved the local smoothing conjecture in all dimensions and derived the Kakeya conjecture and others | Formalized in Lean, materials released |
| Computer science | The exponential time hypothesis (ETH) is false | Formalized in Lean, materials released |
| Physics | A four-dimensional quantum field theory including quantum chromodynamics exists | Outside researchers write an explanation first |
Claims to have overturned the exponential time hypothesis
The result with the greatest impact is in computer science. The exponential time hypothesis is the premise that there is no way to solve, faster than exponential time, the problem of determining whether a logical formula has a satisfying answer (3-SAT), and hundreds of papers in fields such as graph theory and computational biology build on it. OpenAI says it presented a procedure that counts the answers to this problem exactly, faster than exponential time and with less memory. The company itself says, however, that substantial research would be needed to connect this to faster practical procedures.
In mathematics, it says it proved the "local smoothing conjecture," posed in 1991, in all dimensions. Previously, this conjecture had been solved in two dimensions in 2019, and the Kakeya conjecture in three dimensions in 2025. The Verge reported that the consequences for the Kakeya conjecture and others are limited to what was already expected.
OpenAI also commissioned the verifiers
The mathematics and computer science proofs were formalized in Lean, a language for verifying proofs by computer. However, passing in Lean does not necessarily mean the formalized statement matches the claim in the paper.
Verification was entrusted to groups of outside researchers. The computer science group is led by Russell Impagliazzo and Ramamohan Paturi of the University of California, San Diego, and Ryan Williams of the Massachusetts Institute of Technology, and the physics group by Nobel physics laureate David Gross. The physics materials will be released after the outside group writes an explanation. OpenAI says it will pay for meetings held for verification.
At the same time, OpenAI itself acknowledges possible selection bias in having chosen the first verifiers. None of the three results has yet received a third-party verdict.
