Millennium · research open · AMS 35

unsolvedsorry — nobody on it

Existence And Smoothness Of The Navier–Stokes Equation

Conjecture · navier_stokes_existence_and_smoothness_R3

(A) Existence and smoothness of (unforced) Navier–Stokes solutions on ℝ³.

Formal statement · Lean 4.lean
theorem navier_stokes_existence_and_smoothness_R3 (nu : ℝ) (hnu : nu > 0)
    (u₀ : ℝ³ → ℝ³) (hu₀ : InitialVelocityConditionDecay u₀) :
    ∃ v p, NavierStokesExistenceAndSmoothnessRn nu u₀ (f := 0) v p := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗