# OpenAI Claims Its Models Refuted the Exponential Time Hypothesis and Proved Local Smoothing and Yang–Mills Existence; We Found No Independent Verification Yet

Times of AI Desk · 2026-10-27 · Research

[https://timesof.ai/2026/10/openai-claims-eth-refuted-local-smoothing-qft-proofs](https://timesof.ai/2026/10/openai-claims-eth-refuted-local-smoothing-qft-proofs)

> OpenAI said on October 26 that its models refuted the Exponential Time Hypothesis, proved the local smoothing conjecture in every dimension and produced an existence proof for four-dimensional Yang–Mills theory and quantum chromodynamics. The ETH and local smoothing write-ups and Lean proofs are on OpenAI's GitHub; the physics materials are withheld at the physics group's decision, and the Advisory Group on Mathematics and AI has asked OpenAI to publish them. We found no independent verification of any of the three claims.

OpenAI is asking mathematicians, computer scientists and physicists to examine three large claims at once, and the sharpest outside reaction so far comes from mathematicians' own advisory group, which wants the physics material released now. The claims below are OpenAI's, announced **October 26**, and we found no independent verification of any of them.

## The three claims

- **Computer science.** OpenAI says its system "has recently proved that the ETH is false," a result "subsequently verified in Lean." The Exponential Time Hypothesis is a long-standing conjecture about how fast Boolean satisfiability problems can be solved. OpenAI dates the natural-language disproof to October 16 and the Lean formalization to October 17.
- **Mathematics.** OpenAI says its models produced a proof of the local smoothing conjecture, proposed by Sogge in 1991, "in every dimension," and that this also resolves the Kakeya and Stein restriction conjectures in all dimensions. It says the output was obtained on October 18 and formalized in Lean the next day. OpenAI notes that earlier work by Guth, Wang and Zhang covered two dimensions and that Wang and Zahl proved the Kakeya conjecture in three dimensions in 2025.
- **Physics.** OpenAI says its models produced a "mathematically rigorous existence proof" of certain interacting quantum field theories in four dimensions, including quantum chromodynamics and a unified completion of the Standard Model, and that the work includes a proof of the existence of pure Yang–Mills theory, a subproblem of a Clay Mathematics Institute Millennium Prize problem. It says the Yang–Mills proof dates to September 9, the QCD proof to September 18, and that it finished the Lean formalization of Yang–Mills existence on October 16.

## What outside checks exist

For the computer science result, OpenAI says a group led by Russell Impagliazzo and Ramamohan Paturi of UC San Diego and Ryan Williams of MIT will verify and explain the work. OpenAI says the group asked for all raw data to be made public and for OpenAI to fund a conference, and that OpenAI agreed. The natural-language proof and the Lean formalization are on OpenAI's GitHub.

For the physics result, OpenAI says David Gross will lead a group including Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov, and that the group "has decided to hold off on releasing the AI-produced artifacts and instead work on writing it up themselves." The Verge reports that the physics information "has not been released in full." The Advisory Group on Mathematics and Artificial Intelligence, whose members include Timothy Gowers, Martin Hairer and Edward Witten, says OpenAI has said the Lean formalization is complete and that "there is no scientific reason for delaying the release any further." We found no OpenAI response to that call in the sources we read.

For the mathematics result, OpenAI says the external expert it consulted recommended releasing the AI output and leaving researchers to organize their own efforts.

The advisory group published a separate statement on October 25 recommending that AI companies not designate mathematicians to receive output first, citing delayed or unequal access, denied agency, biased selection and borrowed reputation. OpenAI's own post acknowledges that choosing initial shepherds "creates asymmetry of information." [We reported the group's launch in September](https://timesof.ai/2026/09/openai-mathematics-advisory-group) as a roster with a charter that can publish unsolicited criticism.

## What a Lean check does and does not show

OpenAI presents Lean verification for the ETH and local smoothing results and for Yang–Mills existence. Lean confirms that a formal statement follows from the formal proof; it does not confirm that the formal statement captures the written conjecture. [An October 8 update to our report on OpenAI's earlier manuscripts](https://timesof.ai/2026/10/openai-math-722-manuscripts-372-families) covered a Cambridge and King's College London preprint arguing that the Lean formalization of OpenAI's September Navier–Stokes claim does not match its written proof; its authors say they make no claim about whether the written proof is correct. We have not seen a comparable check of the three new formalizations.

## How OpenAI describes the release

OpenAI calls the manuscripts "a form of raw research data" and says it does not seek academic credit for the discoveries. It says working-group participation is voluntary and unpaid, that members are not asked to sign nondisclosure agreements, and that their conclusions are their own. It also points to a $5 million contribution to the Simons Foundation for workshops and programs on understanding AI-produced results.

## Limits

- Every claim in this article is OpenAI's, from its own post; we did not read the proofs or the Lean files and cannot assess their correctness.
- We found no independent verification or refutation of any of the three claims as of October 27.
- OpenAI's post says the local smoothing proof resolves the Kakeya and Stein restriction conjectures in all dimensions. A GitHub release note that The Verge quotes is narrower: it describes the Kakeya maximal and dimension conjectures and Stein's spherical restriction estimates "throughout the interior of the conjectured range." We did not reconcile the two.
- The Verge describes the advisory group as a panel "OpenAI put together." The group's own page says it formed after OpenAI approached some members about an external advisory board, that its members decided to create an independent group instead, and that it operates independently of any AI company and its members take no payment for the work. We use the group's own account.
- The advisory group says its recommendations are intended for mathematics and not necessarily for other areas of science.

## Sources

- [OpenAI: Working with academic communities to build scientific understanding (October 26, 2026)](https://openai.com/index/building-scientific-understanding-with-academic-communities/)
- [Advisory Group on Mathematics and Artificial Intelligence: statements of October 25 and October 26, 2026](https://agmai.org/)
- [The Verge: OpenAI announces three big science discoveries and a new way to work with academics (October 26, 2026)](https://www.theverge.com/ai-artificial-intelligence/1019143/openai-eth-kaseya-science-math-physics)
- [Times of AI: OpenAI Backs a Top-Mathematician Group That Can Publish Unsolicited Criticism (September 21, 2026)](https://timesof.ai/2026/09/openai-mathematics-advisory-group)
- [Times of AI: Update: Paper Says OpenAI’s Lean Navier–Stokes Check Doesn’t Match Its Written Proof, as a New Group Urges Mathematicians to Stop Working With OpenAI (October 7, 2026)](https://timesof.ai/2026/10/openai-math-722-manuscripts-372-families)