OpenAI claims AI proofs of local smoothing, ETH refutation and Yang-Mills existence

OpenAI announced on October 26 that its models produced three major results spanning mathematics, computer science and physics, according to a report on dev.to. The company is explicit that all three claims await independent verification, but if they hold they would mark a turning point for AI-assisted science. The mathematics and computer-science results are accompanied by Lean formalizations published on GitHub; the physics materials are being withheld at the reviewing group's own decision.

Local smoothing settled in every dimension

OpenAI says its models proved the local smoothing conjecture, proposed by Sogge in 1991, in every dimension. The conjecture governs how energy in wave equations concentrates over time, saying that the sharpest concentrations of energy cannot persist for long. Because it sits at the foundation of harmonic analysis, a proof would also settle the Kakeya conjecture — the question of how little space a needle needs in order to point in every direction — and the Stein restriction conjecture in all dimensions.

The company dates the model output to October 18 and its Lean formalization to the following day. It notes that the result builds on earlier work by Guth, Wang and Zhang in two dimensions, and on Wang and Zahl's 2025 proof of the three-dimensional Kakeya conjecture. On external advice, the AI-generated write-up has been released openly on GitHub so that researchers can organize their own checking efforts.

The Exponential Time Hypothesis refuted

The second claim targets the Exponential Time Hypothesis, a long-standing assumption about how hard Boolean satisfiability is to solve, on which hundreds of results in graph theory, computational biology, databases and computational geometry rest. OpenAI says its system showed the hypothesis is false, and that the result was subsequently verified in Lean. The natural-language disproof is dated October 16 and the formalization October 17, both public on GitHub.

A verification group led by Russell Impagliazzo and Ramamohan Paturi of UC San Diego, together with Ryan Williams of MIT, will check and explain the work. The group asked for all raw data to be made public and for OpenAI to fund a conference, and OpenAI agreed to both. If the refutation holds, it reopens the question of how much faster these kinds of computation can actually be made.

Yang-Mills existence and the Standard Model

The third claim is the most consequential. OpenAI says its models produced a mathematically rigorous existence proof for certain interacting quantum field theories in four dimensions, including quantum chromodynamics and a unified completion of the Standard Model, along with a proof that pure Yang-Mills theory exists — a subproblem of a Clay Mathematics Institute Millennium Prize problem.

The Yang-Mills proof is dated September 9, the quantum chromodynamics proof September 18, and the Lean formalization of Yang-Mills existence October 16. Here the release path differs from the other two: a review group led by Nobel laureate David Gross, with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov, has decided to hold back the AI-produced artifacts and write up the work itself.

A split mathematical community

Reaction is divided. The Advisory Group on Mathematics and AI — whose members include Timothy Gowers, Martin Hairer and Edward Witten — says OpenAI has told them the Lean formalization is complete and that there is no scientific reason to delay release any longer. On October 25 the group published a statement criticizing the practice of routing AI output to designated mathematicians first.

Times of AI adds an important caveat: Lean verification establishes that a formal proof follows from a formal statement, not that the formal statement faithfully captures the conjecture as originally written. That distinction, the outlet notes, proved relevant in an earlier OpenAI mathematics manuscript.

Why it matters

Each claim on its own would be significant. Settling local smoothing would resolve three central open problems in harmonic analysis at once; a refutation of the Exponential Time Hypothesis would ripple through complexity theory, unsettling assumptions behind a large body of conditional results; a rigorous existence proof for Yang-Mills would advance one of the Clay Millennium Prize problems. Together, they would be the strongest demonstration yet that AI systems can discover and prove new science rather than merely answer questions about existing knowledge. Just as notable is the process now unfolding around the claims: machine-checkable Lean proofs offer one path to independent verification, while the dispute over how and when AI-generated results are released raises unresolved questions about credit, control and trust in AI-produced science.