OpenAI says its AI proved the Kakeya conjecture, disproved a key complexity hypothesis and showed Yang-Mills theory exists

As of 9:24 a.m. ET, Oct. 27, 2026

OpenAI said Monday that an unreleased internal AI model produced three major results: a proof of a long-open conjecture in harmonic analysis, a disproof of the Exponential Time Hypothesis in computer science, and a rigorous existence proof for quantum field theories that include quantum chromodynamics and pure Yang-Mills theory.

The claims are OpenAI's own and have not been independently verified. The company says outside groups of experts will examine the computer science and physics results, and it has posted the math and computer science manuscripts and their Lean formalizations publicly. Lean is a programming language that checks proofs by machine.

"In our view, these manuscripts are best understood as a form of raw research data," OpenAI said in its announcement.

The math claim: Kakeya and local smoothing

OpenAI says its models produced a proof of Sogge's 1991 local smoothing conjecture, which concerns how waves focus, in every dimension. According to OpenAI, that would also resolve the Kakeya conjecture and Stein's restriction conjecture in all dimensions. The company noted earlier work by others: Guth, Wang and Zhang proved local smoothing in two spatial dimensions in 2019, and Wang and Zahl proved the Kakeya conjecture in three dimensions in 2025.

OpenAI says it obtained the AI output on Oct. 18 and formalized it in Lean the next day. It has released the model's write-up and the Lean proof on GitHub, leaving researchers to organize their own reviews.

The computer science claim: the Exponential Time Hypothesis

The Exponential Time Hypothesis, or ETH, is a widely believed conjecture that Boolean satisfiability problems such as 3-SAT cannot be solved substantially faster than exponential time. OpenAI said it has "been used in hundreds of papers" to derive hardness results. "Surprisingly, our system has recently proved that the ETH is false, a result that was subsequently verified in Lean," the company said.

According to the manuscript description in OpenAI's repository, the paper gives a deterministic algorithm that exactly counts satisfying assignments of fixed-width CNF formulas in subexponential time and polynomial space, and the 3-SAT case refutes the ETH. OpenAI says the AI found the disproof on Oct. 16 and it was formalized in Lean on Oct. 17.

OpenAI said the result will be verified and shepherded by a group led by Russell Impagliazzo and Ramamohan Paturi of UC San Diego, two of the hypothesis's original proposers, and Ryan Williams of MIT. At the group's request, OpenAI said, it made the materials public immediately and committed to funding a conference on the work's implications.

The physics claim: QCD and Yang-Mills

OpenAI says its models produced a mathematically rigorous existence proof for certain four-dimensional interacting quantum field theories with gauge fields and fermions, including QCD and a unified completion of the Standard Model. As a subproblem, OpenAI says, the work includes a proof that pure Yang-Mills theory exists, which it describes as "part of" the Clay Mathematics Institute's Yang-Mills Millennium Prize problem.

OpenAI says the model produced the Yang-Mills proof on Sept. 9 and the QCD proof on Sept. 18, and that it finished a Lean formalization of Yang-Mills existence on Oct. 16. A group led by Nobel laureate David Gross, with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov, will shepherd the physics work, OpenAI said. That group has decided not to release the AI-produced materials for now and to write up the result itself.

Terms of the collaborations

OpenAI said participants in the outside groups are not asked to sign nondisclosure agreements, take part voluntarily and unpaid, and reach their own conclusions. "We do not seek academic credit for the discoveries produced by our internal models," the company said. It pointed to a previously announced $5 million contribution to the Simons Foundation to fund workshops and programs on AI-produced results.

The announcement adds to a large public repository of AI-produced math manuscripts. OpenAI's repository says it holds 721 manuscripts, that "some of the unformalized results could have issues," and that about 42% of top-line results have Lean formalizations. On Oct. 7, OpenAI withdrew three earlier manuscripts after finding a sign error that invalidated one argument, according to the repository's change log.

What is not known

None of the three claims has been confirmed by independent reviewers, and none has gone through peer review. The outside groups have not reported any findings. The physics proof and its Lean formalization have not been made public. Whether the Lean formal statements fully match the conjectures as stated in the research literature has not been independently reviewed. OpenAI has not named or released the model that produced the results.