OpenAI announced on October 26 that internal models produced three research results its own researchers describe as major: a disproof of the Exponential Time Hypothesis, a proof of the local smoothing conjecture in every dimension, and rigorous existence proofs for interacting quantum field theories in four dimensions, including quantum chromodynamics. The company has not named the model behind the work, describing the manuscripts instead as raw research data released for the community to examine.
The computer science claim is the most disruptive of the three. The Exponential Time Hypothesis, conjectured in 1999 by Russell Impagliazzo and Ramamohan Paturi of UC San Diego, underpins hundreds of published hardness results across graph theory, computational biology, databases and computational geometry. OpenAI says its system found the disproof on October 16 and formalized it in the Lean proof assistant the next day. Ryan Williams of MIT summarized the claimed consequence on X: 3SAT on n variables would run in roughly exp(n/(log n)^(1/2+o(1))) time — a sub-exponential bound that, if correct, forces a re-examination of what hundreds of conditional results actually prove.
OpenAI handed verification to an independent group led by Impagliazzo, Paturi and Williams. The three researchers have been explicit about their role: participation is voluntary and unpaid, no NDAs were signed, and their involvement "should not be taken as certification of the claim." All raw data has been made public, and OpenAI agreed to fund conferences on the work's implications, contributing $5 million to the Simons Foundation while claiming no academic credit for itself.
The mathematics result builds on a line of harmonic analysis opened by Christopher Sogge's 1991 local smoothing conjecture, which concerns how long wave energy can concentrate when it focuses. Guth, Wang and Zhang proved the two-dimensional case in 2019, and Wang and Zahl proved the three-dimensional Kakeya conjecture in 2025. OpenAI says its model produced a proof of the local smoothing conjecture in all dimensions on October 18, formalized in Lean on October 19, using a newly constructed auxiliary partial differential equation — a result that would settle the Kakeya and Stein restriction conjectures in every dimension as corollaries.
The physics claim is being handled more conservatively. OpenAI says proofs of Yang-Mills existence were produced on September 9 and of QCD on September 18, with the Yang-Mills formalization finished on October 16. Pure Yang-Mills existence is one half of a Clay Mathematics Institute Millennium Prize problem, though OpenAI does not claim the required mass gap. A review group led by Nobel laureate David Gross, with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov, has chosen not to release the AI-generated material for now and will write up its own account first.
There is an important structural caveat. A Lean formalization only checks a proof against its formal statement; reviewers still need to confirm that each formal statement actually matches the original conjecture. That gap between formalization and meaning is where the three review groups will earn their keep over the coming months.
If the ETH disproof survives scrutiny, the immediate consequence is not faster algorithms but a large debt collection: hundreds of hardness results stated "assuming ETH" would need to be restated or re-derived. OpenAI itself cautions that turning the complexity-theoretic claim into practical speedups remains a substantial open problem. Either way, the episode sets a template for how AI-produced mathematics gets vetted in public — named reviewers, no NDAs, open data and no company credit — that the rest of the industry will likely be judged against.
Comments (0)
Log in to join the discussion
Log InNo comments yet