OpenAI published three results it says were produced by its models, each released with a different plan for turning machine output into human understanding. None names the specific model or system used, and OpenAI explicitly claims no academic credit for the discoveries.
In mathematics, OpenAI reports a proof of Sogge's 1991 local smoothing conjecture in every dimension, built around a novel auxiliary partial differential equation. Because local smoothing implies them, that would also settle the Kakeya conjecture and Stein's restriction conjecture in all dimensions. For context, Guth, Wang and Zhang proved local smoothing in two spatial dimensions in 2019, and Wang and Zahl proved Kakeya in three dimensions in 2025. The output was obtained on October 18, formalized in Lean the next day, and released as a Lean proof on GitHub plus a model-written preprint dated October 25. On expert advice, OpenAI released the raw output and left the community to organize its own exposition.
In computer science, OpenAI says its system disproved the Exponential Time Hypothesis, the conjecture that satisfiability of Boolean formulas cannot be solved in subexponential time, which underpins conditional hardness results in hundreds of papers. The natural-language disproof was found on October 16 and verified in Lean on October 17. Russell Impagliazzo and Ramamohan Paturi, who proposed the hypothesis, and Ryan Williams of MIT will shepherd independent verification. OpenAI committed to releasing all raw data and funding a conference, and the page notes that turning the refutation into faster practical algorithms will need significant further research.
In physics, OpenAI reports a rigorous existence proof for interacting four-dimensional quantum field theories with gauge fields and fermions, including quantum chromodynamics and the simplest grand unified theory containing the Standard Model's fields, building on Balaban's constructive program. It includes pure Yang–Mills existence, a subproblem tied to the Clay Millennium Prize. Here only the Yang–Mills existence proof is stated to be Lean-formalized; a group led by David Gross, with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov, is withholding the artifacts and writing the work up itself.
Why it matters: if these hold, they would be the first resolutions of long-standing flagship problems in analysis, complexity theory and mathematical physics attributed primarily to AI, and the ETH refutation in particular would ripple through fine-grained complexity. The caveats are substantial. External verification is described as future work, the page calls the manuscripts raw research data, Lean formalization is only as strong as the fidelity of the formal statements to the intended conjectures, and the QCD result has no formal proof yet. OpenAI also announced a five million dollar contribution to the Simons Foundation for workshops on AI-produced results.