OpenAI says its models proved the local smoothing conjecture, refuted the Exponential Time Hypothesis and proved Yang–Mills existence

OpenAI announced three results in mathematics, computer science and physics produced by its models. Everything below is OpenAI's own claim; none has been independently verified yet, and OpenAI says the results were checked in Lean.

• Mathematics (harmonic analysis). OpenAI says its models proved the local smoothing conjecture in every dimension, which it says also resolves the Kakeya conjecture and Stein's restriction conjecture in all dimensions, via a novel auxiliary partial differential equation. It released the models' natural-language write-up and a Lean proof in its public openai/math GitHub repository, following the approach of its October 6 release.
• Computer science. OpenAI says its system disproved the Exponential Time Hypothesis (ETH), a conjecture about the complexity of Boolean formula satisfiability, and that the disproof was verified in Lean. Ryan Williams will lead a group with Russell Impagliazzo and Ramamohan Paturi (who with Francis Zane proposed the ETH) to verify and explain it. At the group's request, OpenAI has made the natural-language proof and the Lean formalization public.
• Physics. OpenAI says its models produced a mathematically rigorous existence proof of certain four-dimensional interacting quantum field theories with gauge fields and fermions, including QCD and a unified completion of the Standard Model, and as a subproblem a proof of existence of pure Yang–Mills theory, part of the Clay Mathematics Institute's Millennium Prize problem. It says the proofs are formally verified in Lean. A group led by David Gross, with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov, will shepherd the work, and OpenAI will defer to them on releasing materials.

OpenAI describes the manuscripts as "raw research data" and says it asked external experts to act as shepherds, who advised a different release strategy for each result. It gives these dates for the work: the local smoothing output on October 18 (formalized in Lean the next day), the ETH disproof on October 16 (formalized October 17), and the Yang–Mills existence proof on September 9 (QCD on September 18, with the Lean formalization of Yang–Mills finished October 16). The physics group asks that communications go to a dedicated email address and has decided to hold back the AI-produced artifacts while it writes the work up itself.

OpenAI says the collaborations follow four principles: transparency (no nondisclosure agreements), no academic credit sought by OpenAI, recognition for the groups, and independence (participation is voluntary and unpaid, and members speak only for themselves). It says it will fund a conference on the ETH result and points to its recent $5 million contribution to the Simons Foundation for workshops and programs on AI-produced results. It also made small changes to the GitHub repository, listed in its history file. The announcement thread on X had 405 points and 30 comments on X by the evening of October 26.