oai-math-revised beta

Browse › Real and complex analysis › 079 Local smoothing for the Euclidean wave equation

Local smoothing for the Euclidean wave equation

OpenAI · October 25, 2026

Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion

Edit NOTES.md · Existing issues · Source on GitHub

Abstract

We prove Sogge’s local smoothing conjecture for the Euclidean wave equation in every spatial dimension at least two. We deduce the Bochner–Riesz conjecture, maximal estimates for these means, and sharp bounds for Stein’s square function. We obtain Fourier restriction estimates for the sphere, the compact paraboloid, and the truncated cone throughout the interior of the conjectured range, as well as local smoothing for the Schrödinger equation. We also prove the Kakeya and Nikodym maximal conjectures. In particular, every Euclidean Kakeya set has full Hausdorff dimension.

If the PDF does not display here, open it directly: Open PDF.

Notes

No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-27) and not checked by a person. May be wrong or incomplete. Report an error.

Comments and discussion

  • James Leng (@JamesLeng15), post on X (2026-10-27). Notes that the proof is only about 25 pages, relies primarily on elliptic PDEs and "does not use much of the mathematics developed by the harmonic analysis lineage".

Formalization

  • OpenAI math release, Lean scope notes for family 079 (lean/docs/079.md). The release's scope note for both papers says the Lean development covers half-wave local smoothing for all $n\ge2$ and $2\le p<\infty$ with $\varepsilon$-loss, plus strict-range Bochner–Riesz, spherical extension, Stein square-function and Kakeya maximal/Hausdorff-dimension statements, with comparator links to LocalSmoothing.lean. [family-level]

Possibly relevant literature (found by the agent, not checked)

Digests and expositions

  • AI Proved What?, Local smoothing in every dimension? OpenAI's wave equation claim (Episode 079, 2026-10-26). Explains the claimed all-dimensional theorem, its consequences and proof outline, discusses the September three-dimensional companion paper, reports the site's own numerical checks, and says no expert review has been named. [family-level] [AI-generated per source]
  • Closed Form, Local smoothing for the Euclidean wave equation (Closed Form, accessed 2026-10-27). Explains the fixed-time versus time-averaged Sobolev thresholds with numerical examples, distinguishes the September three-dimensional and October all-dimensional claims, and summarizes their consequences and listed formalization scope. [AI-generated per source] [family-level]

News and blogs

Elsewhere

Independent sites; their content is not reviewed here.

Cite

@misc{OAI:Local-smoothing-for-the-Euclidean-wave-equation-October-25-2026,
  author = {{OpenAI}},
  title = {{Local smoothing for the Euclidean wave equation}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Local-smoothing-for-the-Euclidean-wave-equation-October-25-2026/paper.pdf}{OAI:Local-smoothing-for-the-Euclidean-wave-equation-October-25-2026}},
  year = {2026}
}

Lean formalization

OpenAI provides Lean files for this family. The scope note, lean/docs/079.md, says which results they cover.

Each result is stated in a file in lean/ComparatorChallenges/. These files end in sorry on purpose: they only state the result. The proof is in a separate module, and Lean's comparator is the tool for checking that the module proves exactly what the statement file says.

Nobody has checked whether the Lean statements say what the paper claims.

Family 079: Local smoothing for the Euclidean wave equation

Proves Sogge’s local smoothing conjecture in every spatial dimension $n\ge2$, with arbitrarily small loss above the sharp Sobolev threshold. The wave estimate yields the Bochner–Riesz conjecture and, for $2\le p\lt\infty$, maximal bounds for these means and sharp bounds for Stein’s square function. It also gives Fourier restriction throughout the interior of the conjectured range for the sphere, compact paraboloid, and truncated cone, and local smoothing for the Schrödinger equation. The Kakeya and Nikodym maximal conjectures follow. In particular, every Euclidean Kakeya set has full Hausdorff dimension.

Other papers in this family: