Partial differential equations · Result 371

Stable blowup for the defocusing Schrödinger equation

1 paperLean

For a sufficiently large odd nonlinearity power, constructs a nonempty open set of initial data in \(H^k(\mathbb T^{12})\), with k > 8, whose solutions of the scalar defocusing nonlinear Schrödinger equation blow up in finite time. Thus finite-time blowup is stable under Sobolev perturbations in this supercritical regime.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Stable self-similar blowup for a supercritical defocusing Schrödinger equation on the torus

OpenAI · September 24, 2026

We prove stable self-similar finite-time blowup for a supercritical defocusing nonlinear Schrödinger equation on the twelve-dimensional torus. For a sufficiently large odd power, the blowup initial data contain a nonempty open set in a high Sobolev space. As a consequence, Gaussian Fourier initial data of arbitrarily high Sobolev regularity can have positive probability of finite-time blowup.

Read PDF Download Source

Cite

@misc{OAI:Stable-Self-Similar-Blowup-for-a-Supercritical-Defocusing-Schrodinger-Equation-on-the-Torus-September-24-2026,
  author = {{OpenAI}},
  title = {{Stable self-similar blowup for a supercritical defocusing Schr{\"o}dinger equation on the torus}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Stable-Self-Similar-Blowup-for-a-Supercritical-Defocusing-Schrodinger-Equation-on-the-Torus-September-24-2026/paper.pdf}{OAI:Stable-Self-Similar-Blowup-for-a-Supercritical-Defocusing-Schrodinger-Equation-on-the-Torus-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Stable self-similar blowup for a supercritical defocusing Schrödinger equation on the torus

Scope

The formalization constructs stable self-similar finite-time blowup for defocusing nonlinear Schrödinger equations on the twelve-dimensional torus. For every prescribed lower bound on the power, it selects an odd power at least that large and a Sobolev index \(k>8\) for which a nonempty open set of \(H^k\) initial data has the stated classical blowup behavior. The selected quantifier gives arbitrarily large odd powers, rather than every sufficiently large odd power.

For each such construction, Gaussian Fourier data with decay exponent \(\alpha>k+6\) assign positive probability to the blowup set, and almost-sure global existence fails. The exponent \(\alpha\) may be arbitrarily large.

Comparator links

Result	Comparator statement
Stable self-similar blowup and positive-probability Gaussian blowup	DefocusingNLS.lean

Scope note on GitHub →