Stability Framework for the Singularity of the Euler Equations on $\mathbb{R}^3$
Valentin Duruisseaux, Adarsh Ganeshram, Robert J. George, Anima Anandkumar
math.AP
Sep 9, 2026 · v2
math.NA
TL;DR
Proof steps are marked as formalized and verified in Lean via a companion LeanPDE effort using Mathlib and TorchLean, alongside Julia/Arb numerical certificates.
Abstract
In a recent numerical study, we found a high-precision singular profile for the Euler equations on the unbounded domain $\mathbb{R}^3$. The present manuscript complements that study by establishing in detail a preliminary framework for proving (nonlinear) stability of the approximate self-similar profile, reducing the analysis to a large but finite collection of explicit estimates and computable constants. Conditional on rigorous certification of the estimates and constants appearing in the argument, and on the candidate profile satisfying the required nonlinear stability conditions, the framework closes the stability proof and, crucially, allows the resulting stable rescaled profile to be reconstructed as an admissible solution in the original variables that becomes singular in finite physical time. With the overall stability and reconstruction mechanisms formulated, the remaining work within this approach is largely quantitative: determining whether the explicit constants and margins can be rigorously certified with sufficient positive margin and, where necessary, sharpening selected analytic estimates.
Problem
Whether smooth initial data for the 3D Euler equations on unbounded R^3 can develop a finite-time singularity remains open. A prior numerical study found a high-precision approximate self-similar blowup profile, but its nonlinear stability had not been established.
Approach
The authors use a dynamic rescaling formulation of the axisymmetric Euler equations, under which the approximate profile becomes a steady state with modulation parameters. They build coupled low- and high-order weighted energy estimates for the perturbation dynamics, with weights and tunable parameters optimized numerically. Every constant is explicit or computable by a prescribed rigorous procedure using splines, interval arithmetic and certified matrix bounds. Symbolic derivations and proof steps are formalized in Lean with Mathlib and TorchLean, while the numerical certificates are produced separately in Julia with Arb.
Results
Nonlinear stability is reduced to a finite set of explicit quantitative conditions. If these are certified with positive margin, the stability proof closes and the profile can be reconstructed as an admissible solution that becomes singular in finite physical time. Rigorous certification of the constants remains future work.
