Navier-Stokes existence and smoothness

A foundational regularity problem for the equations governing fluid flow.

Analysis Partial differential equations Fluid mechanics

Mathematical statement

For three-dimensional incompressible flow, determine whether $\partial_tu+(u\cdot\nabla)u=-\nabla p+\nu\Delta u$ with $\nabla\cdot u=0$ always has a global smooth solution, or exhibit finite-time breakdown.

Statement source: Therefore editorial statement

Statement terms: Source-specific

Editorial wording by Therefore. No statement reuse license is granted.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

MillenniumNavierStokes.clay_prize_navier_stokes

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem clay_prize_navier_stokes :    ClayNavierStokes := by  sorry

Statement source: Lean Millennium Prize Problems
Lean version: v4.31.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Clay Mathematics Institute problem pageofficial Navier-Stokes existence and smoothness overviewbackground