The Navier-Stokes equations describe how fluids move. Every ocean current, every weather pattern, every blood flow through an artery, every turbulent wake behind an aircraft — all governed by these equations, written down nearly two centuries ago.
The equations are deceptively simple. A velocity field $u(x,t)$ tells you how fast the fluid is moving at each point. Viscosity $\nu$ smooths the flow. Pressure $p$ enforces incompressibility (the fluid doesn't compress). The nonlinear term $(u \cdot \nabla)u$ — the fluid carrying itself — is where the difficulty lives.
The question the Clay Mathematics Institute asks, and offers $1,000,000 for, is this:
Given any smooth, physically reasonable initial velocity field in three dimensions, does a smooth solution to the Navier-Stokes equations exist for all future time? Or can the fluid develop a singularity — a point where velocity becomes infinite?
In two dimensions, the answer is yes: smooth solutions exist forever (Ladyzhenskaya, 1969). In three dimensions, despite 90 years of effort by some of the finest mathematicians alive, nobody knows.
The answer involves a phenomenon called vortex stretching. In 2D, vorticity (the local spinning of the fluid) is a scalar quantity pointing perpendicular to the plane. It can be transported and diffused, but it cannot stretch. In 3D, vorticity is a vector that can be amplified by the velocity gradient — vortex tubes can be stretched thinner and spin faster, concentrating energy into smaller scales.
Viscosity fights back: it dissipates energy, especially at small scales where gradients are steep. The Millennium Prize asks whether viscosity always wins this fight, or whether the nonlinear cascade can concentrate energy faster than viscosity can dissipate it.
In Fourier space, the energy of the fluid is distributed across modes (wavenumbers). The Gevrey norm $G_\sigma$ measures this energy with an exponential weight that emphasizes high-frequency modes:
When $G_\sigma$ is finite for some $\sigma > 0$, the velocity field is real-analytic — as smooth as a function can possibly be. The regularity problem becomes: does $G_\sigma$ stay finite, or can it blow up?
The evolution of $G_\sigma$ is governed by two competing forces:
The viscous term (grade 2) is always stabilizing — it removes energy. The advective term (grade 3) can go either way — it's the vortex stretching in disguise. The entire Millennium Prize reduces to one question: does grade 2 always control grade 3?
This is not an abstract exercise. The Navier-Stokes equations are used every day by hundreds of thousands of engineers and scientists. Understanding their mathematical structure has direct consequences:
Weather prediction is fundamentally a Navier-Stokes problem. Every improvement in understanding fluid regularity translates to better bounds on prediction error, better turbulence models, and more reliable climate projections.
Blood flow through arteries, air flow through lungs, cerebrospinal fluid dynamics — all governed by Navier-Stokes. Understanding when and how singularities can form (or cannot) informs the design of artificial hearts, stents, and ventilators.
Aircraft design, wind turbine optimization, combustion engine efficiency, building aerodynamics — the practical world runs on computational fluid dynamics, which runs on approximations to Navier-Stokes. Mathematical guarantees about solution regularity translate to guarantees about simulation accuracy.
Turbulence is sometimes called "the last great unsolved problem of classical physics." Kolmogorov's 1941 theory gives statistical predictions for turbulent cascades, but a rigorous derivation from the Navier-Stokes equations remains out of reach. Solving the regularity problem would be the first step toward a rigorous theory of turbulence.
The Navier-Stokes equations have a remarkably long history. Here are the milestones that define the field.
Navier derives the first viscous fluid model from molecular hypotheses.
Stokes reformulates the equations in modern continuum mechanics form.
Global weak solutions. Leray proves that 3D Navier-Stokes always has at least one "weak solution" — a generalized notion of solution that may not be smooth. The question of whether these solutions are actually smooth remains open.
Hopf extends Leray's construction to bounded domains.
Local strong solutions. Fujita and Kato prove that smooth solutions exist for short time (or for all time if the initial data is small).
2D is solved. Ladyzhenskaya proves global regularity in two dimensions. The 3D problem remains open.
Partial regularity. Caffarelli, Kohn, and Nirenberg prove that any potential singular set has fractal (parabolic Hausdorff) dimension at most 1. Singularities, if they exist, are extremely rare.
Gevrey regularity. Foias and Temam show that solutions are real-analytic and develop the completing-the-square technique for Gevrey energy bounds.
Millennium Prize. The Clay Mathematics Institute designates Navier-Stokes existence and smoothness as one of seven Millennium Prize Problems, with a $1,000,000 prize.
$L^3$ endpoint regularity. If a solution stays bounded in the critical $L^3$ norm, it remains smooth. The sharpest conditional result known.
Barrier result. Tao shows that an "averaged" version of 3D Navier-Stokes can blow up, proving that purely energy-based methods cannot solve the problem. The structure of the nonlinearity matters.
Weak non-uniqueness. Buckmaster and Vicol show that below the energy class, Navier-Stokes has non-unique solutions. The uniqueness question is as hard as the regularity question.
3D Euler blow-up. Chen and Hou give a computer-assisted proof that 3D Euler equations (Navier-Stokes without viscosity) develop singularities. This is the first rigorous proof of blow-up for an incompressible 3D fluid equation.
Leray-Hopf non-uniqueness. Hou, Wang, and Yang prove that even "physical" (Leray-Hopf) solutions to unforced 3D Navier-Stokes are non-unique. Multiple solutions can emerge from the same initial condition.
The dominant trend in 2024–2026 has been negative results: singularities form in the inviscid case (Euler), solutions are non-unique, and purely energy-based methods face fundamental barriers. The question of whether viscosity prevents blow-up in 3D remains wide open.
Most leading groups are working on negative directions: showing that blow-up occurs (for related equations), that solutions are non-unique, or that certain proof strategies cannot work. This is valuable — understanding what fails is essential to understanding what might succeed.
Our approach is different: we are building the positive case, step by step, in a machine-verified framework where every claim is checkable. If regularity holds, our infrastructure will prove it. If it fails, our framework will identify precisely where and why — which axiom cannot be closed, which estimate breaks down.
Formal verification of PDE theory is almost nonexistent. The closest prior work is the formalization of basic Sobolev spaces in Coq (Bréhard et al., 2024). The Gagliardo-Nirenberg-Sobolev inequality was recently merged into Lean's Mathlib. No prior project has formalized any Navier-Stokes regularity result in any proof assistant.
We are building a machine-checked formalization of Navier-Stokes regularity theory in Lean 4, a modern proof assistant backed by the Mathlib mathematical library. Every theorem is verified by a computer. Every axiom (unproved assumption) is explicitly named, counted, and audited.
Our central tool is a grade decomposition of the Gevrey energy balance. The evolution of the analytic energy splits cleanly into two terms:
Our formalization contains a three-phase proof path:
Transparency is central to this project. Here is the exact status:
Verified: 190+ theorems/lemmas in Lean 4. Zero sorry (incomplete proofs).
Axioms: 12 explicitly named assumptions, all encoding standard textbook results
(Picard-Lindelöf, Gronwall, Aubin-Lions compactness, Fatou's lemma).
None represent open mathematical problems.
Files: 14 Lean source files covering Gevrey norms, trilinear bounds,
conditional regularity, 2D vanishing, 3D analysis, completing-the-square, and the
Millennium closure theorem.
Not claimed: A complete proof of the Millennium Prize. The 12 axioms are
not yet proved in Lean. What we have is a verified reduction: if the axioms hold
(and they encode known mathematics), the Prize follows.
The history of claimed Navier-Stokes proofs is littered with errors — some subtle, some not. Machine verification eliminates an entire class of mistakes: if the Lean code compiles, the logical chain from axioms to conclusion is correct. The remaining question is only whether the axioms themselves are true (and for standard textbook results, they are).
This approach also produces a precise, auditable record. Every axiom is named. Every dependence is tracked. Anyone can clone the repository and verify the entire chain. This is what mathematical transparency looks like in 2026.