Overview
- OpenAI announced Monday that its internal models produced three claimed discoveries: a proof in harmonic analysis, a disproof of the Exponential Time Hypothesis, and existence proofs for certain four‑dimensional quantum field theories.
- For mathematics, OpenAI says the models produced a proof of Sogge’s local smoothing conjecture that it formalized in the Lean proof assistant and published on GitHub, and it asserts this also resolves the Kakeya and Stein restriction conjectures.
- OpenAI says the computer‑science result—produced on October 16 and formalized in Lean the next day—gives a deterministic algorithm that refutes ETH, and a working group led by Russell Impagliazzo, Ramamohan Paturi, and Ryan Williams will examine the claim.
- The physics claim covers mathematically rigorous existence proofs for interacting four‑dimensional quantum field theories including QCD, but OpenAI has deferred full public release while a team led by David Gross prepares a shepherded writeup.
- Experts warn Lean checks only confirm formal derivations not that the formal statements match the canonical problems, AGMAI criticized the ‘shepherd’ access model, competing AI lab claims increase urgency, and independent verification and provenance disclosure could take months.