Non-Uniqueness of Weak Solutions to the Unforced Two-Dimensional Euler Equations with Vorticity in $L^1\cap L^p$

Does Yudovich's uniqueness theorem extend below bounded vorticity? For the unforced two-dimensional incompressible Euler equations, is a weak solution with vorticity in $L^\infty_t L^p_x$ , $p<\infty$ , uniquely determined by its initial vorticity, in particular for large $p$ ? Bruè, Colombo and Kumar call this a central question (on $\mathbb{T}^2$ , with velocity in $L^2$ ); without force it was open for every $p$ beyond the small $p>1$ reached by their convex integration.

Result: Proved(see note)
Status: Variant only
AI contribution: AI co-developed
Method: Computation
Field: Partial Differential Equations
Posed by: Folklore since Yudovich's theorem; stated as a central question in Bruè, Colombo and Kumar, Flexibility of two-dimensional Euler flows with integrable vorticity, Section 1.1.1 (arXiv:2408.07934, 2024)
Year posed: —
Years open: —
Solved: 2026-10-22
Model: Claude Opus 5.5
Vendor: Anthropic
Collaborators: Matei P. Coiculescu
Verification: Lean-checked, statement unaudited
Publication: Preprint
Significance: 50 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Claims to settle the question in the plane: an explicit radial datum $f\ge0$ , in $(L^1\cap L^q)(\mathbb{R}^2)$ for all $q<\infty$ and not bounded, has two distinct renormalized weak solutions in $L^\infty_t(L^1\cap L^q)_x$ for every $q\in(4/3,\infty)$ : the stationary $f$ and a 3-fold symmetric solution equimeasurable with $f$ . No force. Open: $q\le4/3$ ; finite energy (the velocity is not in $L^2$ , as $f$ has nonzero circulation); vanishing viscosity; $\mathbb{T}^2$ . Caveats: the spectral input (N1)-(N2) is computer-assisted; Part II is a draft; no independent expert review; the Lean proof is kernel-checked modulo a compiled checker run, its statement read here but not independently anchored. A concurrent fully AI-generated claim (Pappalettera-Sorella, Hexagon; finite energy, $p>2$ ) predates Part I; a later human paper (Hou, Qin, Song, Zhang, arXiv 2610.40552) gives a related dichotomy.

What the AI did

Claude Opus 5.5 (Anthropic) largely produced the detailed proofs and estimates of Part I: the compactness criterion for non-uniqueness and the linear analysis of the ring (mode decomposition, Evans function, eigenvalue bounds, semigroup estimates). It also wrote most of the text, the interval-arithmetic verification code used in Part II, and the Lean 4 formalization of the full proof. The author checked all proofs in Part I by hand.

Verification

No independent mathematician has checked this yet. Read by this site on 3 November 2026 at commit bd6a6c0 of the GitHub repository, not rebuilt (about 1,280 Lean files, 170,000 lines, Lean 4.34.0-rc2 with mathlib; a build takes hours and the checker run 8.75 hours). A grep of every .lean file found no sorry, admit, axiom or opaque declarations, native_decide, implemented_by, extern or unsafe outside comments. The statement layer was read: MainTheorem states the headline as in Theorem 1.1 (two distinct renormalized weak solutions in $L^\infty_t(L^1\cap L^q)_x$ for every $q\in(4/3,\infty)$ , one stationary, from a radial nonnegative unbounded datum in every $L^q$ ), with the true Biot-Savart kernel, a standard weak formulation against smooth compactly supported test functions, DiPerna-Lions renormalization and distinctness as failure of a.e. equality. The kernel-checked main_theorem_of_certificate is conditional on check cert = true, established by running the compiled checker ncert (log in the repository), so that step trusts the Lean compiler, runtime and GMP, as native_decide would. The axiom list is the author's, not re-run here. No independent anchor (Formal Conjectures, a tracker) exists for this statement. Part II, with the nonlinear construction, is a draft not on arXiv. The Python/Arb certificate was not re-run here.

Sources

PaperarXivPart II draft (not on arXiv)
Lean proofGitHub: manuscript, Lean formalization and Arb certificate (Coiculescu)
Lean statementLean statement: MainTheoremLean statement: weak and renormalized weak solutions
CodeInterval-arithmetic certificate (Python/Arb)
Independent workConcurrent related result (LLM-generated): Pappalettera–Sorella
Problem recordBruè, Colombo, Kumar, Section 1.1.1: the question
OtherLater related: Hou, Qin, Song, Zhang, neutral vortex arrays

Submitted by StormyStoat567 on 23 Oct 2026

Non-Uniqueness of Weak Solutions to the Unforced Two-Dimensional Euler Equations with Vorticity in L1∩LpL^1\cap L^pL1∩Lp

What was actually shown

What the AI did

Verification

Sources

Discussion

Non-Uniqueness of Weak Solutions to the Unforced Two-Dimensional Euler Equations with Vorticity in $L^1\cap L^p$