Formal Mathematics · Mathematical Physics · Computational Fluid Dynamics

Navier-Stokes & Euler in Lean 4

A dual-track mathematical research system: machine-checked formal verification of the 3D incompressible Navier-Stokes and Euler equations in the Lean 4 theorem prover, alongside high-precision pseudospectral Runge-Kutta numerical simulations investigating finite-time singularity blowup candidates.

Source on GitHub → Lean 4 Prover Mathlib v4 Python Pseudospectral RK4 11 Tests Passing
Theorem Prover
Lean 4
Checked against Mathlib v4
Energy Invariant
Proven
Formal Euler.lean theorem
Blowup Scaling
\(\tau^{-1/2-h}\)
Anisotropic needle core
Kinetic Energy
\(\to 0\)
Bounded (Millennium Prop C)

1. Mathematical Theory & Formal Theorems

By the Beale-Kato-Majda (BKM) criterion, a smooth classical solution \(u \in C([0, T^*); H^s)\) ceases to exist at \(T^*\) if and only if accumulated vorticity diverges:

Beale-Kato-Majda Blowup Criterion

\[ \int_0^{T^*} \|\omega(\cdot, t)\|_{L^\infty} \, dt = \infty \]

A central mathematical challenge in 3D fluid singularities is constructing blowup candidates that maintain finite initial kinetic energy. In classical isotropic self-similar profiles (\(\ell_r \sim \ell_z \sim \tau^{1/2}\)), the kinetic energy diverges. Our formalization analyzes an anisotropic contraction where the radial scale \(\ell_r \sim \tau^{1/2}\) contracts faster than the axial scale \(\ell_z \sim \tau^{1/2-h}\):

\[ E_{\text{core}}(t) = \int_{\text{core}} |u|^2 \, dx \sim \ell_r^2 \cdot \ell_z \cdot \|u\|_{L^\infty}^2 \sim \tau^1 \cdot \tau^{1/2-h} \cdot \tau^{-1-2h} = \tau^{1/2-3h} \xrightarrow[\tau \to 0]{} 0 \]

For \(0 < h < 1/6\), core kinetic energy decays strictly to zero as the vortex contracts into an infinitely thin rotating needle with bounded global energy.

2. Live Interactive Pseudospectral Fluid Vortex Simulator

Simulate fluid vorticity advection and singularity scaling in real time. Adjust the Reynolds number, time-to-blowup \(\tau = 1 - t\), and anisotropy perturbation \(h\) to observe core thinning and velocity amplification:

Vortex Core & Singularity Particle Visualizer

Real-time particle advection under Burgers vortex dissipation

Re: 2,500 · Active Vortices: 140
Velocity Scale (\(u_\theta\))
3.55×
Scaling as \(\tau^{-1/2-h}\)
Core Aspect (\(\ell_r / \ell_z\))
0.89
Scaling as \(\tau^h \to 0\) (Needle)
Core Energy (\(E\))
0.45 (Decaying)
Bounded as \(\tau^{1/2-3h} \to 0\)