← All problems

∇
Clay Millennium Problem

Navier–Stokes Global Regularity

Do smooth initial conditions always give smooth global solutions to the 3D incompressible Navier–Stokes equations?

Progress

60%
Conditional framework verified
Current approach
Grade decomposition of Gevrey energy balance; conditional regularity via machine-checked Sobolev embedding chains.
Status notes
Full proof architecture Lean-checked. Remaining gap: unconditional Gevrey-class bootstrap from grade-2 decay.

Direct contributions

1 paper
Formal Verification Working Paper Lean DOI Flagship
Grade Decomposition and Gevrey Regularity for Navier-Stokes: A Machine-Checked Conditional Framework
We introduce a grade decomposition of the Gevrey energy balance for the incompressible Navier-Stokes equations. The physically correct model uses $\mathbb{C}$-valued Fourier coefficients with a factor of $i$ in the advection; the real-coefficient model trivializes all grade-3 terms.
9,471 words 7 claims