Overview
- OpenAI announced on Monday, Oct. 26 that its internal models produced a Lean‑formalized proof of the local smoothing conjecture that the company says also resolves the Kakeya and Stein restriction conjectures, a claimed refutation of the Exponential Time Hypothesis, and mathematically rigorous existence proofs for certain four‑dimensional quantum field theories.
- The math and computer‑science artifacts and natural‑language explanations are published on GitHub with Lean proofs that check each logical step, while the quantum‑field theory materials are being withheld while a David Gross‑led group prepares a writeup.
- OpenAI assigned independent academic 'shepherds' to guide verification: Russell Impagliazzo, Ramamohan Paturi and Ryan Williams for the ETH claim and David Gross and other senior physicists for the QFT work, and it has pledged funding and workshops to support community review.
- Experts warn that Lean verification only proves that a formal statement follows from given assumptions and does not by itself show the formal statement matches the standard conjectures or reveal training‑data provenance, so months of independent checking and adjudication by journals and institutions will be needed.
- If validated, the results would force wide technical reassessments because the ETH underpins many fine‑grained hardness results, the local smoothing/Kakeya claims reshape harmonic‑analysis foundations, and rigorous four‑dimensional QFT proofs would touch core problems in mathematical physics.