OpenAI said on October 26 that it released a natural-language writeup and a Lean formalization for what it describes as an AI-generated proof of Sogge’s 1991 local smoothing conjecture for the Euclidean wave equation.
The public record is split between the OpenAI announcement and the linked GitHub history, and the two describe the scope a bit differently. OpenAI’s post says the result proves the conjecture in every dimension and therefore resolves the Kakeya conjecture and Stein’s restriction conjecture in all dimensions. The GitHub history page is narrower: it says the result covers waves in every spatial dimension at least two, yields Kakeya maximal and dimension conjectures, and gives Stein’s spherical restriction estimates throughout the interior of the conjectured range.
That matters because the proof artifacts are public and inspectable, but the scope should be read from both sources together rather than from the launch post alone.