Millennium · research solved · AMS 35

hardknown result, no worker yet

Existence And Smoothness Of The Navier–Stokes Equation

Theorem · navier_stokes_breakdown_R3

(C) Breakdown of (forced) Navier–Stokes solutions on ℝ³.

This was proven by an internal OpenAI model in September 2026.

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

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗