Motivation

The incompressible Navier–Stokes equations are the standard model for the motion of a viscous fluid such as water or air, used daily in engineering, meteorology and oceanography. Yet the most basic mathematical question about them is open: starting from smooth initial data in three dimensions, does a smooth solution exist for all time? This is one of the seven Millennium Prize Problems of the Clay Mathematics Institute. Its official formulation is Charles Fefferman's problem description, Existence and smoothness of the Navier–Stokes equation (2000), which offers a prize for a proof of any one of four statements: global existence and smoothness on $\mathbb{R}^3$ (statement (A)) or on the torus $\mathbb{R}^3/\mathbb{Z}^3$ (statement (B)), or a counterexample to either (statements (C) and (D)). This mission formalizes statement (A), together with the classical partial results that Fefferman lists as known.

Timeline.

• 1822–1845: Navier and Stokes write down the equations of a viscous incompressible fluid.
• 1934: Jean Leray, Sur le mouvement d'un liquide visqueux emplissant l'espace (Acta Math. 63), proves on $\mathbb{R}^3$ that smooth solutions exist for a positive time depending on the data, that they exist for all time when the data is small compared with the viscosity, and that global weak solutions with finite energy always exist. Their smoothness and uniqueness are left open.
• 1933–1969: the two-dimensional problem is settled (Leray for the plane; Olga Ladyzhenskaya's monograph The Mathematical Theory of Viscous Incompressible Flow, 2nd ed. 1969, for bounded domains): smooth solutions exist for all time and are unique.
• 1984: Tosio Kato, Strong $L^p$-solutions of the Navier–Stokes equation in $\mathbb{R}^m$ (Math. Z. 187), gives global solutions for initial data small in $L^3(\mathbb{R}^3)$.
• 1976–1998: partial regularity. Scheffer, then Caffarelli, Kohn and Nirenberg (Comm. Pure Appl. Math. 35, 1982), show that the singular set of a suitable weak solution has one-dimensional parabolic Hausdorff measure zero.
• 2000: the Clay Mathematics Institute adopts Fefferman's formulation as a Millennium Prize Problem. It remains open.

Setting

Fix a dimension $n \ge 1$ and write $\mathbb{R}^n$ for Euclidean $n$-space with its Euclidean norm $|x|$; in Lean this is NavierStokes.Vec n. A velocity field assigns to each time $t \in \mathbb{R}$ and point $x \in \mathbb{R}^n$ a vector $u(x,t) \in \mathbb{R}^n$; in Lean $u\,t$ is the field at time $t$ and $u\,t\,x$ is Fefferman's $u(x,t)$. A pressure is a real function $p(x,t)$. The viscosity $\nu$ is a positive constant. The external force of Fefferman's equation (1) is identically zero throughout, as in statement (A).

For a vector field $v : \mathbb{R}^n \to \mathbb{R}^n$ the divergence is

$$\operatorname{div} v = \sum_{i=1}^n \frac{\partial v_i}{\partial x_i},$$

in Lean NavierStokes.div, computed from the Fréchet derivative $Dv(x)$ as $\sum_i (Dv(x)\,e_i)_i$. The Laplacian $\Delta v = \sum_i \partial^2 v/\partial x_i^2$ acts componentwise (Mathlib's Laplacian on inner product spaces). The gradient $\nabla p$ is Mathlib's gradient. The convective term $\sum_j u_j\,\partial u/\partial x_j$ is the derivative of $u(\cdot,t)$ at $x$ in the direction $u(x,t)$. Finally $|\nabla v|^2 = \sum_{i,j} (\partial v_i/\partial x_j)^2$ is NavierStokes.gradNormSq.

Admissible initial data (Fefferman's condition (4), NavierStokes.IsInitialData): a $C^\infty$, divergence-free vector field $u^0$ that decays together with all its derivatives faster than any power,

$$|\partial_x^\alpha u^0(x)| \le C_{\alpha K}\,(1+|x|)^{-K} \quad \text{on } \mathbb{R}^n, \text{ for every } \alpha \text{ and } K.$$

In Lean the bound is $(1+|x|)^K\,\|D^k u^0(x)\| \le C_{kK}$ on the $k$-th Fréchet derivative, an equivalent family of conditions. These are exactly the divergence-free Schwartz functions.

A physically reasonable solution on a set $S$ of times (NavierStokes.IsSolutionOn; $S = [0,\infty)$ for NavierStokes.IsSolution) is a pair $(u,p)$ such that

1. (Fefferman (6)) $u$ and $p$ are $C^\infty$ on $S \times \mathbb{R}^n$, up to the boundary of $S$;
2. (Fefferman (1), $f \equiv 0$) for every $t \in S$ with $t > 0$ and every $x$,

$$\frac{\partial u}{\partial t} + \sum_{j=1}^n u_j \frac{\partial u}{\partial x_j} = \nu\,\Delta u - \nabla p;$$

3. (Fefferman (2)) $\operatorname{div} u(\cdot,t) = 0$ for every $t \in S$;
4. (Fefferman (3)) $u(x,0) = u^0(x)$;
5. (Fefferman (7), bounded energy) $\int_{\mathbb{R}^n} |u(x,t)|^2\,dx < C$ for all $t \in S$, for some constant $C$.

Formalization targets

Goal: Fefferman's statement (A)

Take $\nu > 0$ and $n = 3$. For every admissible initial datum $u^0$ there exist a velocity field $u$ and a pressure $p$ forming a physically reasonable solution on $\mathbb{R}^3 \times [0,\infty)$:

$$\forall\, \nu > 0,\ \forall\, u^0 \text{ satisfying (4)},\ \exists\, (u,p) \text{ satisfying (1), (2), (3), (6), (7) on } \mathbb{R}^3 \times [0,\infty).$$

This is NavierStokes.existence_and_smoothness_R3. It is open; a proof would settle the Millennium Prize Problem in the affirmative.

Milestones: what Fefferman lists as known

1. Local existence (NavierStokes.local_existence_R3): for $n = 3$ and every admissible $u^0$ there are $T > 0$ and a physically reasonable solution on $\mathbb{R}^3 \times [0,T)$. Fefferman: "(A) and (B) hold ... if the time interval $[0,\infty)$ is replaced by a small time interval $[0,T)$, with $T$ depending on the initial data."
2. Global existence for small data (NavierStokes.small_data_global_existence_R3): there is an absolute constant $c > 0$ such that, for $n = 3$, (A) holds for every admissible $u^0$ with

$$\|u^0\|_{L^2}^2\,\|\nabla u^0\|_{L^2}^2 \le c\,\nu^4.$$

Fefferman: "(A) and (B) hold provided the initial velocity $u^0$ satisfies a smallness condition." The scale-invariant product is Leray's form of the condition; it implies smallness of $\|u^0\|_{L^3}/\nu$, so Kato's theorem also applies. 3. The two-dimensional case (NavierStokes.existence_and_smoothness_R2): statement (A) with $n = 2$. Fefferman: "In two dimensions, the analogues of assertions (A) and (B) have been known for a long time (Ladyzhenskaya)."

A bridging lemma, NavierStokes.isInitialData_iff_schwartz, identifies the admissible data with the divergence-free elements of Mathlib's Schwartz space.

Significance

The result itself. Statement (A) asks whether the basic model of viscous flow is well posed in the classical sense, i.e. whether smooth finite-energy flows can develop singularities in finite time. A positive answer shows the equations never leave the classical regime; a negative one shows the model predicts its own breakdown. Fefferman: "since we don't even know whether these solutions exist, our understanding is at a very primitive level."

Formalizing it. None of the results in this mission has a machine-checked proof, and Mathlib contains no theory of the Navier–Stokes or Euler equations. The milestones are all proved in the literature; formalizing them requires building, on Mathlib's calculus, measure theory and Schwartz space, the heat semigroup on $\mathbb{R}^n$, the pressure equation $\Delta p = -\sum_{i,j} \partial_i\partial_j(u_i u_j)$ or the Leray projection, energy estimates, and a fixed-point construction of solutions, most of which is reusable for other evolution equations. The goal is open and expected to remain so; its role is to fix in Lean the exact statement the prize asks for, so partial results are formalized against it.

Difficulty

The energy identity $\frac{d}{dt}\int|u|^2 = -2\nu\int|\nabla u|^2$ controls $u$ in $L^2$ and $\nabla u$ in $L^2_{t,x}$, but in three dimensions this control is supercritical: under the scaling $u_\lambda(x,t) = \lambda u(\lambda x, \lambda^2 t)$ that preserves the equations, the energy of $u_\lambda$ shrinks as $\lambda \to \infty$, so bounded energy does not prevent concentration at small scales. Every known continuation criterion (Leray, Prodi–Serrin, Beale–Kato–Majda, Escauriaza–Seregin–Šverák) needs a quantity at or above critical scaling, none of which the energy controls. The obvious first idea, an ordinary differential inequality for $\|\nabla u(t)\|_{L^2}$, gives $\frac{d}{dt}\|\nabla u\|_{L^2}^2 \le C\nu^{-3}\|\nabla u\|_{L^2}^6$, which closes only for small data or short time. That is exactly why milestones 1 and 2 are theorems and the goal is not.

The formalization adds a second difficulty: the solutions of the literature live in Sobolev or Besov spaces, with pointwise smoothness of $u$ and $p$ recovered afterwards by regularity theory, and Mathlib has neither Sobolev spaces on $\mathbb{R}^n$ nor the heat semigroup in usable form.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure; the dimension is a parameter, the goal fixes $n = 3$ and the 2D milestone $n = 2$.
• A velocity field is a function of all real times, but every condition is imposed only on the time set $S$; values at negative times are unconstrained.
• Smoothness on $\mathbb{R}^n \times [0,\infty)$ is Mathlib's ContDiffOn of the uncurried map on the closed half-space, i.e. all derivatives extend continuously to $t = 0$. The momentum equation is imposed at interior times $t > 0$ with two-sided derivatives; by continuity of the derivatives this is equivalent to Fefferman's "$t \ge 0$".
• Derivatives are Mathlib's total functions (fderiv, deriv, iteratedFDeriv, gradient, Laplacian) with junk value $0$ at non-differentiable points; the smoothness hypotheses make every derivative in the statements honest.
• The energy is a Lebesgue integral in $[0,\infty]$, equal to $\infty$ when $u(\cdot,t) \notin L^2$, so bounded energy cannot hold vacuously. The $L^2$ norms in the small-data hypothesis are Bochner integrals, genuine for Schwartz data.
• No normalization is imposed on the pressure, as in Fefferman's text.

No trivializing formalization. The zero field solves the equations only for $u^0 = 0$; for any other admissible $u^0$ the initial condition, smoothness, the equation on $t > 0$ and bounded energy must all hold.

Infrastructure needed and welcome contributions. The heat kernel on $\mathbb{R}^n$ with Schwartz bounds; the Riesz-transform representation of the pressure or the Leray projection; energy identities for smooth decaying solutions; local existence by Picard iteration; the two-dimensional vorticity equation and its maximum principle. Theorems in the NavierStokes namespace, decompositions of the milestones, and Mathlib lemmas about ContDiffOn on half-spaces are all welcome. Statements (B), (C), (D) and the Euler equations ($\nu = 0$) are out of scope.

Selected references

• C. L. Fefferman, Existence and smoothness of the Navier–Stokes equation, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf
• J. Leray, Sur le mouvement d'un liquide visqueux emplissant l'espace, Acta Mathematica 63 (1934), 193–248. https://doi.org/10.1007/BF02547354
• O. A. Ladyzhenskaya, The Mathematical Theory of Viscous Incompressible Flow, 2nd ed., Gordon and Breach, 1969. https://archive.org/details/mathematicaltheo0000lady
• T. Kato, Strong $L^p$-solutions of the Navier–Stokes equation in $\mathbb{R}^m$, with applications to weak solutions, Mathematische Zeitschrift 187 (1984), 471–480. https://doi.org/10.1007/BF01174182
• L. Caffarelli, R. Kohn, L. Nirenberg, Partial regularity of suitable weak solutions of the Navier–Stokes equations, Communications on Pure and Applied Mathematics 35 (1982), 771–831. https://doi.org/10.1002/cpa.3160350604
• A. J. Majda, A. L. Bertozzi, Vorticity and Incompressible Flow, Cambridge University Press, 2002. https://doi.org/10.1017/CBO9780511613203
• J. C. Robinson, J. L. Rodrigo, W. Sadowski, The Three-Dimensional Navier–Stokes Equations: Classical Theory, Cambridge University Press, 2016. https://doi.org/10.1017/CBO9781139095143