OpenAI said on Oct. 26 it generated proofs for three longstanding conjectures in mathematics, computer science and physics and verified them in Lean.
The lab framed the manuscripts as raw research data and said it is testing how to turn that data into scientific understanding. It assigned a different release strategy to each result in consultation with external shepherds.
For harmonic analysis, the models claim a proof of Sogge's 1991 local smoothing conjecture in every dimension, which OpenAI said also resolves the Kakeya and Stein restriction conjectures in all dimensions. The lab said the AI output appeared Oct. 18, 2026 and was formalized in Lean the next day, building on Guth, Wang and Zhang's 2019 proof in two dimensions and Wang and Zahl's 2025 proof of Kakeya in three dimensions.
For complexity theory, the models claim the Exponential Time Hypothesis is false. The conjecture, that 3-SAT cannot be solved in subexponential time, has anchored hardness for hundreds of papers in graph theory, computational biology, databases and geometry. Independent coverage noted the same framing, that ETH has been widely believed true and concerns Boolean satisfiability closely tied to P versus NP, per The Next Web.
That last claim is the one that forces a workflow change. Any team whose lower bound or fine-grained hardness argument assumes ETH must now audit that dependency. Impagliazzo and Paturi, who proposed ETH with Francis Zane, plus Ryan Williams of MIT will lead a verification group, OpenAI said. The lab said it will publish the natural language proof and Lean formalization on GitHub and fund a conference to map implications.
Physics follows a tighter gate. The models claim a rigorous construction of four-dimensional gauge theories with fermions, including QCD and a unified completion of the Standard Model, with pure Yang-Mills as a subproblem that falls under the Clay Millennium Prize formulation by Jaffe and Witten. The lab said the Yang-Mills draft appeared Sept. 9, the QCD draft Sept. 18, and Lean formalization finished Oct. 16. Release is deferred to a group led by David Gross, with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov, who will coordinate via [email protected].
OpenAI said participants will not sign nondisclosure agreements, will not be paid, will receive recognition for expository work, and will not speak for the company. It said it will turn over artifacts to each group, complementing a $5 million contribution to the Simons Foundation to support workshops. The split strategy is itself the test. One track is fully public from day one, one is public but shepherded, one is held back until experts rewrite it. The lab acknowledged the tradeoff: early shepherds shape who sees information first.
Skepticism remains operational, not theoretical. Lean checking confirms formal correctness of the encoded statements, not whether definitions match the intended conjectures or whether hidden assumptions slipped into formalization. That review now sits with the appointed groups and the broader community, with the math and CS artifacts already on GitHub and the physics rewrite still to come.
