feat(Navier-Stokes): formalization of Navier–Stokes existence and smoothness #1457

lecopivo · 2026-01-03T18:16:46Z

Formalization of Navier-Stokes existence and smoothness problem as described in https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf

Potentially issues:

not immediately obvious that fderiv ℝ (v · t) x (v x t) is the convective term and that div is divergence
the growth conditions uses ‖iteratedFDeriv ℝ n v₀ x‖ instead of |∂^α u(x,t)| but it should be equivalent
at various places I'm not completely sure if there should be t ≥ 0 or t > 0 as fderiv might not give what we think at t=0. Mainly in NavierStokesExistenceAndSmoothness.navierStokes

Note:

I didn't use the unicode character nu for viscosity as it looks too similar to the letter v which is used for velocity.
bikeshead: should it use v(x,t)(aligned with the official statement) or v(t,x) that is more mathlib aligned?
should it be formulated in an arbitrary dimension and then instantiated for n:=3?

…othness

google-cla · 2026-01-03T18:16:50Z

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

…her minor issues

YaelDillies

Could you add way more documentation? I would make sure we're at least at mathlib standard (every def has a docstring), and hopefully go even further by writing down explicitly all the design decisions you've taken.

I didn't use the unicode character nu for viscosity as it looks too similar to the letter v which is used for velocity.

This seems fine.

bikeshead: should it use v(x,t) (aligned with the official statement) or v(t,x) that is more mathlib aligned?

I don't mind, so long as the discrepancy is clearly documented.

should it be formulated in an arbitrary dimension and then instantiated for n:=3?

Sure! That seems very reasonable so long as it isn't too difficult to do so. I assume it's already solved for n = 2? If so, it seems reasonable to have one statement for n = 2, one for n = 3 and one for all n, the first one being solved and the other two open.

FormalConjectures/Wikipedia/NavierStokes.lean

- added doc strings, mostly AI generated but cleaned up and removed fluff - using notation form EuclideanGeometry

lecopivo · 2026-01-03T22:41:49Z

@YaelDillies Hopefully, I have addressed all the issues.

The docs strings are mostly AI generated but they sound good to me and I don't really know what else I would write there.

YaelDillies · 2026-01-04T14:31:52Z

FormalConjectures/Millenium/NavierStokes.lean

+  (v₀ : ℝ³ → ℝ³) (hv₀ : InitialVelocityConditionRn v₀) :
+  ∃ v p, NavierStokesExistenceAndSmoothnessRn (n:=3) nu v₀ (f:=0) v p := sorry


Suggested change

(v₀ : ℝ³ → ℝ³) (hv₀ : InitialVelocityConditionRn v₀) :

∃ v p, NavierStokesExistenceAndSmoothnessRn (n:=3) nu v₀ (f:=0) v p := sorry

(v₀ : ℝ³ → ℝ³) (hv₀ : InitialVelocityConditionRn v₀) :

∃ v p, NavierStokesExistenceAndSmoothnessRn (n:=3) nu v₀ (f:=0) v p := sorry

Same below

YaelDillies · 2026-01-04T14:32:05Z

FormalConjectures/Millenium/NavierStokes.lean

+
+/--


Suggested change

/--

/--

YaelDillies · 2026-01-04T14:36:46Z

FormalConjectures/Millenium/NavierStokes.lean

+This condition ensures the velocity field has finite energy and reasonable
+behavior as |x| → ∞.
+-/
+structure InitialVelocityConditionRn {n : ℕ} (v₀ : ℝ^n → ℝ^n) : Prop


What about

Suggested change

structure InitialVelocityConditionRn {n : ℕ} (v₀ : ℝ^n → ℝ^n) : Prop

structure InitialVelocityConditionDecay {n : ℕ} (v₀ : ℝ^n → ℝ^n) : Prop

instead? In both cases, the function has domain R^n, so Rn is a bit confusing as a way to distinguish

YaelDillies · 2026-01-04T15:23:05Z

FormalConjectures/Millenium/NavierStokes.lean

+/-- (A) Existence and smoothness of Navier–Stokes solutions on ℝ³. -/
+@[category research open, AMS 35]
+theorem navier_stokes_existence_and_smoothness_R3 (nu : ℝ) (hnu : nu > 0)
+  (v₀ : ℝ³ → ℝ³) (hv₀ : InitialVelocityConditionRn v₀) :


The source uses

Suggested change

(v₀ : ℝ³ → ℝ³) (hv₀ : InitialVelocityConditionRn v₀) :

(u₀ : ℝ³ → ℝ³) (hv₀ : InitialVelocityConditionRn u₀) :

instead. Maybe you could do that so that nu can become \nu?

YaelDillies · 2026-01-04T15:29:06Z

FormalConjectures/Millenium/NavierStokes.lean

+  /-- The pressure is periodic in space with period 1 for all times t ≥ 0 (condition 10). -/
+  pressure_periodic : ∀ t ≥ 0, IsPeriodic (p · t)


Technically, the periodicity of pressure isn't stated anywhere. Could you leave a comment to that effect?

Errata on page 6 says also $p$ should be periodic.

YaelDillies · 2026-01-04T15:36:49Z

FormalConjectures/Millenium/NavierStokes.lean

+  /-- The Navier-Stokes equation (equation 1):
+      ∂v/∂t + (v·∇)v = ν∆v - ∇p + f -/
+  navier_stokes : ∀ x, ∀ t > 0,
+    deriv (v x ·) t + fderiv ℝ (v · t) x (v x t) = nu • Δ (v · t) x - gradient (p · t) x + f x t


Condition 1 is also stated for t = 0. Could you explain the discrepancy in a comment?

YaelDillies · 2026-01-04T15:40:11Z

FormalConjectures/Millenium/NavierStokes.lean

+    (v :  ℝ^n → ℝ → ℝ^n) (p : ℝ^n → ℝ → ℝ) : Prop
+  extends NavierStokesExistenceAndSmoothness nu v₀ f v p where
+
+  /-- The velocity is square-integrable at each time t ≥ 0. -/


Suggested change

/-- The velocity is square-integrable at each time t ≥ 0. -/

/-- The velocity is square-integrable at each time t ≥ 0 (condition 7). -/

YaelDillies · 2026-01-04T15:52:45Z

FormalConjectures/Millenium/NavierStokes.lean

+  ∃ (v₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³),
+    InitialVelocityConditionRn v₀ ∧ ForceConditionRn f ∧
+    ¬(∃ v p, NavierStokesExistenceAndSmoothnessRn (n:=3) nu v₀ f v p) := sorry


Suggested change

∃ (v₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³),

InitialVelocityConditionRn v₀ ∧ ForceConditionRn f ∧

¬(∃ v p, NavierStokesExistenceAndSmoothnessRn (n:=3) nu v₀ f v p) := sorry

∃ (v₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³),

InitialVelocityConditionRn v₀ ∧ ForceConditionRn f ∧

\forall v p, ¬ NavierStokesExistenceAndSmoothnessRn (n:=3) nu v₀ f v p := sorry

maybe?

FormalConjectures/Millenium/NavierStokes.lean

mirefek · 2026-01-08T18:53:34Z

We looked at it with Tomáš Bárta (teacher of ODE at Charles University), and it looks good to us.

mirefek · 2026-01-09T17:44:42Z

More from Tomáš Bárta:

the formulation of NS seems correct to me but I have some remarks:

Should there be 'for all nu>0' in all theorems?

It seems strange that there is 'for all nu' in parts A, B (existence of global smooth solutions) and also 'for all nu' in parts C, D (non-existence of globally defined smooth solutions). In fact, if non-existence is proved for one nu, by a rescaling procedure it is proved for all positive nu (with another v_0 and f). So, it does not matter whether there is 'for all nu' or 'there exists nu'. But may be it would be better to write 'there exists nu>0' in parts C, D? I suggest to ask an NS expert concerning this.

Problems with $t>0$ and $t\ge 0$.

The present lean formulation writes $t>0$ in some conditions instead of $t\ge 0$ and the reason seems to be the language. Why don't you use iteratedFDerivWithin instead of iteratedFDeriv. Wouldn't it allow to work on $t\ge 0$? Maybe this would be a more elegant solution. (iteratedFDerivWithin seems to be used in definition of ContDiffOn, so we need it anyway)

grunweg

Thanks for your PR. With Moritz Firsching sitting next to me (to answer any formal conjectures questions), I just took a first look, until line 130. Most of my comments are minor or stylistic --- but let me echo the comment about t > 0 vs t >= 0.

grunweg · 2026-01-20T14:18:38Z

FormalConjectures/Millenium/NavierStokes.lean

+The divergence of a vector field `v : ℝⁿ → ℝⁿ` at point `x`,
+computed as the trace of the Jacobian matrix.
+
+In coordinates: div v = Σᵢ ∂vᵢ/∂xᵢ


This formula should be written as a LaTeX formula; likewise for the formula three lines above and in the other doc-strings below.

grunweg · 2026-01-20T14:22:31Z

FormalConjectures/Millenium/NavierStokes.lean

+In coordinates: div v = Σᵢ ∂vᵢ/∂xᵢ
+-/
+noncomputable
+def divergence {n : ℕ} (v : ℝ^n → ℝ^n) (x : ℝ^n) : ℝ := (fderiv ℝ v x).trace ℝ (ℝ^n)


This definition has junk value zero when v is not differentiable at x (because then the fderiv is defined to be zero).

Maybe also add that as a simp lemma. And some basic API lemmas, such as linearity?

grunweg · 2026-01-20T14:25:24Z

FormalConjectures/Millenium/NavierStokes.lean

+noncomputable
+def divergence {n : ℕ} (v : ℝ^n → ℝ^n) (x : ℝ^n) : ℝ := (fderiv ℝ v x).trace ℝ (ℝ^n)
+
+notation "∇⬝" => divergence


Suggested change

notation "∇⬝" => divergence

@[inherit_doc]

notation "∇⬝" => divergence

Can you also mention the notation in the doc-string, please?

You're only using this notation once. Can you also use it on line 75 --- or remove it?

grunweg · 2026-01-20T14:25:47Z

FormalConjectures/Millenium/NavierStokes.lean

+with period 1, i.e., `f(x + eᵢ) = f(x)` for each unit vector `eᵢ`.
+This captures functions on the n-torus ℝⁿ/ℤⁿ.
+-/
+def IsPeriodic {α : Sort*} {n : ℕ} (f : ℝ^n → α) : Prop :=


Perhaps rename this to IsOnePeriodic?

grunweg · 2026-01-20T14:30:41Z

FormalConjectures/Millenium/NavierStokes.lean

+  /-- All derivatives of v₀ decay faster than any polynomial (condition 4).
+
+      For any derivative order m and any decay rate K, there exists a constant C
+      such that |∂ᵐv₀(x)| ≤ C/(1+|x|)^K. -/


Personal preference, to some extent:

Suggested change

/-- All derivatives of v₀ decay faster than any polynomial (condition 4).

For any derivative order m and any decay rate K, there exists a constant C

such that |∂ᵐv₀(x)| ≤ C/(1+|x|)^K. -/

/-- All derivatives of v₀ decay faster than any polynomial (condition 4).

For any derivative order m and any decay rate K, there exists a constant C

such that |∂ᵐv₀(x)| ≤ C/(1+|x|)^K. -/

(and please apply the LaTeX formatting also)

grunweg · 2026-01-20T14:33:03Z

FormalConjectures/Millenium/NavierStokes.lean

+/--
+Initial velocity conditions for the periodic Navier-Stokes problem on ℝⁿ/ℤⁿ.
+
+The velocity must be smooth, divergence-free, and periodic with period 1


I also like the phrasing "1-periodic"; this may read more nicely. Optional/subjective.

grunweg · 2026-01-20T14:34:39Z

FormalConjectures/Millenium/NavierStokes.lean

+-/
+structure InitialVelocityConditionPeriodic {n : ℕ} (v₀ : ℝ^n → ℝ^n) : Prop
+  extends InitialVelocityCondition v₀ where
+  /-- The initial velocity is periodic with period 1 in each direction (condition 8) -/


This is only part of condition 8 --- perhaps rephrase as "condition 8, part 1"? Same above.

grunweg · 2026-01-20T14:34:51Z

FormalConjectures/Millenium/NavierStokes.lean

+  periodic : IsPeriodic v₀
+
+/--
+Basic smoothness condition on external forcing term.


Please add a definite article here. Thanks!

grunweg · 2026-01-20T14:35:52Z

FormalConjectures/Millenium/NavierStokes.lean

+The force must be smooth and decay faster than any polynomial
+in both space and time (condition 5 in Fefferman's paper).
+-/
+structure ForceConditionRn {n : ℕ} (f : ℝ^n → ℝ → ℝ^n) : Prop


style: I'd put the extends clause on the same line. (Also, please apply the style comments about doc-string formatting in the same way as above.)

grunweg · 2026-01-20T14:40:29Z

FormalConjectures/Millenium/NavierStokes.lean

+      For any derivative orders m and decay rate K, there exists C such that
+      |∂ᵐ_{x,t} f(x,t)| ≤ C/(1+|x|+t)^K for t > 0.
+  -/
+  decay : ∀ m : ℕ, ∀ K : ℝ, ∃ C : ℝ, ∀ x, ∀ t > 0,


I have the same comment as was made in the thread above: please use t >= 0 (and iteratedFDerivWithin if needed) --- or say clearly why you think this is a bad idea. I don't see why. Also below (and in the doc-string).

grunweg

I finished my review: another collection of minor items; no further big questions.

grunweg · 2026-01-21T15:11:41Z

FormalConjectures/Millenium/NavierStokes.lean

+-/
+
+open ContDiff Set InnerProductSpace MeasureTheory EuclideanGeometry
+


Should n be a global implicit variable?

grunweg · 2026-01-21T15:12:48Z

FormalConjectures/Millenium/NavierStokes.lean

+structure ForceConditionPeriodic {n : ℕ} (f : ℝ^n → ℝ → ℝ^n) : Prop
+  extends ForceCondition f where
+  /-- The force is periodic in space with period 1 for all times (condition 8) -/
+  periodic : ∀ t ≥ 0, IsPeriodic (f · t)


I'd name this field isPeriodic (or isOnePeriodic if you rename IsPeriodic to IsOnePeriodic)

grunweg · 2026-01-21T15:14:34Z

FormalConjectures/Millenium/NavierStokes.lean

+structure NavierStokesExistenceAndSmoothness {n : ℕ}
+    (nu : ℝ) (v₀ : ℝ^n → ℝ^n) (f : ℝ^n → ℝ → ℝ^n)
+    (v :  ℝ^n → ℝ → ℝ^n) (p : ℝ^n → ℝ → ℝ) : Prop where
+


Suggested change

grunweg · 2026-01-21T15:17:30Z

FormalConjectures/Millenium/NavierStokes.lean

+    (nu : ℝ) (v₀ : ℝ^n → ℝ^n) (f : ℝ^n → ℝ → ℝ^n)
+    (v :  ℝ^n → ℝ → ℝ^n) (p : ℝ^n → ℝ → ℝ) : Prop
+  extends NavierStokesExistenceAndSmoothness nu v₀ f v p where
+


Suggested change

grunweg · 2026-01-21T15:23:03Z

FormalConjectures/Millenium/NavierStokes.lean

+  extends NavierStokesExistenceAndSmoothness nu v₀ f v p where
+
+  /-- The velocity is square-integrable at each time t ≥ 0. -/
+  integrable : ∀ t ≥ 0, Integrable (‖v · t‖^2)


Should this use MemLp instead, i.e.

Suggested change

integrable : ∀ t ≥ 0, Integrable (‖v · t‖^2)

integrable : ∀ t ≥ 0, MemLp (‖v · t‖) 2

grunweg · 2026-01-21T15:24:05Z

FormalConjectures/Millenium/NavierStokes.lean

+  extends NavierStokesExistenceAndSmoothness nu v₀ f v p where
+
+  /-- The velocity is periodic in space with period 1 for all times t ≥ 0 (condition 10). -/
+  velocity_periodic : ∀ t ≥ 0, IsPeriodic (v · t)


I'd name this as isPeriodic_velocity (following mathlib conventions). Similarly below.

grunweg · 2026-01-21T15:26:29Z

FormalConjectures/Millenium/NavierStokes.lean

+  integrable : ∀ t ≥ 0, Integrable (‖v · t‖^2)
+
+  /-- The kinetic energy ∫|v(x,t)|²dx remains uniformly bounded for all time (condition 7). -/
+  globally_bounded_energy : ∃ E, ∀ t ≥ 0, (∫ x : ℝ^n, ‖v x t‖^2) < E


This is the Lebesgue integral, right? Then everything is fine. (For the Bochner integral, you'd have to worry about junk values.)

grunweg · 2026-01-21T15:28:42Z

FormalConjectures/Millenium/NavierStokes.lean

+theorem navier_stokes_breakdown_periodic (nu : ℝ) (hnu : nu > 0) :
+  ∃ (v₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³),
+    InitialVelocityConditionPeriodic v₀ ∧ ForceConditionPeriodic f ∧
+    ¬(∃ v p, NavierStokesExistenceAndSmoothnessPeriodic (n:=3) nu v₀ f v p) := sorry


Spaces around :=, please --- also above.

lecopivo added 2 commits January 3, 2026 18:59

feat(Navier-Stokes): formalization of Navier–Stokes existence and smo…

452204e

…othness

feat: add equation numbers from the PDF file

6c3482a

lecopivo added 2 commits January 3, 2026 19:25

fix: style fix

1a2f284

fix: replace implication with conjunction in breakdown and fix few ot…

f0b3654

…her minor issues

lecopivo mentioned this pull request Jan 3, 2026

Navier–Stokes existence and smoothness #1462

Open

1 task

YaelDillies reviewed Jan 3, 2026

View reviewed changes

FormalConjectures/Wikipedia/NavierStokes.lean Outdated Show resolved Hide resolved

FormalConjectures/Wikipedia/NavierStokes.lean Outdated Show resolved Hide resolved

FormalConjectures/Wikipedia/NavierStokes.lean Outdated Show resolved Hide resolved

YaelDillies added ams-35: Partial differential equations awaiting-author The author should answer a question or perform changes. Reply when done. labels Jan 3, 2026

lecopivo added 3 commits January 3, 2026 23:25

- generalized to n-dimensions

01af728

- added doc strings, mostly AI generated but cleaned up and removed fluff - using notation form EuclideanGeometry

moved to a dedicaded folder

499ea04

fix copyright message

576d81e

YaelDillies added millenium-problems Clay Maths Institute Millenium Problems and removed awaiting-author The author should answer a question or perform changes. Reply when done. labels Jan 4, 2026

YaelDillies reviewed Jan 4, 2026

View reviewed changes

YaelDillies added the awaiting-author The author should answer a question or perform changes. Reply when done. label Jan 4, 2026

Paul-Lez self-requested a review January 5, 2026 22:28

mirefek mentioned this pull request Jan 12, 2026

Navier Stokes misformalization lean-dojo/LeanMillenniumPrizeProblems#4

Open

grunweg reviewed Jan 20, 2026

View reviewed changes

grunweg reviewed Jan 21, 2026

View reviewed changes

		(v₀ : ℝ³ → ℝ³) (hv₀ : InitialVelocityConditionRn v₀) :
		∃ v p, NavierStokesExistenceAndSmoothnessRn (n:=3) nu v₀ (f:=0) v p := sorry

	structure InitialVelocityConditionRn {n : ℕ} (v₀ : ℝ^n → ℝ^n) : Prop
	structure InitialVelocityConditionDecay {n : ℕ} (v₀ : ℝ^n → ℝ^n) : Prop

	(v₀ : ℝ³ → ℝ³) (hv₀ : InitialVelocityConditionRn v₀) :
	(u₀ : ℝ³ → ℝ³) (hv₀ : InitialVelocityConditionRn u₀) :

		/-- The pressure is periodic in space with period 1 for all times t ≥ 0 (condition 10). -/
		pressure_periodic : ∀ t ≥ 0, IsPeriodic (p · t)

	/-- The velocity is square-integrable at each time t ≥ 0. -/
	/-- The velocity is square-integrable at each time t ≥ 0 (condition 7). -/

	notation "∇⬝" => divergence
	@[inherit_doc]
	notation "∇⬝" => divergence

		-/

		open ContDiff Set InnerProductSpace MeasureTheory EuclideanGeometry

	integrable : ∀ t ≥ 0, Integrable (‖v · t‖^2)
	integrable : ∀ t ≥ 0, MemLp (‖v · t‖) 2

feat(Navier-Stokes): formalization of Navier–Stokes existence and smoothness #1457

Are you sure you want to change the base?

feat(Navier-Stokes): formalization of Navier–Stokes existence and smoothness #1457

Uh oh!

Conversation

lecopivo commented Jan 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

google-cla bot commented Jan 3, 2026

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

lecopivo commented Jan 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mirefek commented Jan 8, 2026

Uh oh!

mirefek commented Jan 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

lecopivo commented Jan 3, 2026 •

edited

Loading

lecopivo commented Jan 3, 2026 •

edited

Loading

mirefek commented Jan 9, 2026 •

edited

Loading