The Navier-Stokes Equations

Imagine watching smoke curl from a candle, or water swirl down a drain. The motion looks impossibly complex, but since the 19th century mathematicians and physicists have modeled fluid flow with the Navier-Stokes equations.

These equations describe how fluids (liquids and gases) move by tracking velocity, pressure, viscosity (roughly, internal friction), and applied forces. In regimes where the model applies and the initial data are known, they are extraordinarily successful at predicting real flows.

The open problem is narrower and more precise: in three dimensions, can every smooth starting flow remain smooth for all future time, or can singularities form?

The incompressible Navier-Stokes equations on $\mathbb{R}^3$ are

$$\partial_t u + (u \cdot \nabla)u = -\nabla p + \nu \Delta u + f,$$

$$\nabla \cdot u = 0, \qquad u(x,0) = u_0(x),$$

where $u : \mathbb{R}^3 \times [0,T) \to \mathbb{R}^3$ is the velocity field, $p : \mathbb{R}^3 \times [0,T) \to \mathbb{R}$ is the pressure, $\nu > 0$ is the kinematic viscosity, and $f$ is an external force.

For the Clay Millennium problem on $\mathbb{R}^3$, one usually takes $f \equiv 0$ and asks about smooth divergence-free initial data whose derivatives decay rapidly at infinity. The question is whether such data always generate a unique global smooth solution for every $t \ge 0$, or whether smoothness can fail in finite time.

The Navier-Stokes equations are central to aerodynamics, weather prediction, ocean modeling, and blood-flow simulation. Engineers and scientists use them every day.

What remains unproved is not whether the equations are useful, but whether every smooth 3D initial state leads to a smooth solution for all time. Global weak solutions are known to exist, but in three dimensions we still do not know whether smooth solutions can break down or whether weak solutions are always unique.

This question is so fundamental that the Clay Mathematics Institute named it one of seven Millennium Prize Problems in 2000, with a $1 million prize for a correct solution.

The regularity problem sits at a nexus of several deep mathematical threads:

• Weak versus smooth solutions — Leray (1934) proved existence of global weak solutions in the energy class, but global smoothness and uniqueness for arbitrary smooth 3D data remain open.
• Turbulence and concentration — any proof of global regularity, or any genuine finite-time singularity, would sharply constrain how enstrophy and smaller-scale structure can concentrate in turbulent flow.
• Computation — numerical simulations resolve many physically relevant regimes, but finite-resolution computation alone cannot settle whether singularities are impossible or unavoidable.

The Clay problem asks for a proof of global smoothness for all smooth, divergence-free, rapidly decaying data on $\mathbb{R}^3$ with $f \equiv 0$, or else a counterexample; an equivalent periodic formulation on $\mathbb{T}^3$ is also accepted.

This site breaks the Navier-Stokes problem into digestible pieces:

• The Millennium Problem — what Clay is actually asking, precisely stated
• Why It's Hard — the core mathematical difficulties, explained intuitively
• Subproblems — how the big question decomposes into tractable pieces
• Approaches — the main strategies mathematicians have tried
• Our Proof page — a placeholder for an in-progress approach and formalization effort, not a completed published proof

Use the Intuitive / Formal toggle in the top bar to switch between an intuitive overview and fuller mathematical detail on any page.

This site provides a structured overview of the regularity problem and its landscape:

• The Millennium Problem — the precise Clay formulation and what constitutes a valid solution
• Why It's Hard — supercriticality, the nonlinear term, scaling barriers, and the gap between energy estimates and critical control
• Subproblems — partial regularity, conditional regularity criteria, blowup scenarios, and critical norms
• Approaches — Leray-Hopf theory, Caffarelli-Kohn-Nirenberg partial regularity, vorticity criteria, and critical-space methods
• Our Proof page — currently an in-progress placeholder for ongoing ideas and Lean 4 formalization work, rather than a completed formal proof

Toggle between Intuitive and Formal modes using the switch in the navigation bar.