Navier–Stokes existence and smoothness

Overview

Current assessment

OpenAI reports smooth forced breakdown in the whole space and on the three-torus, with full formal endpoints. The new arguments are under assessment; unforced regularity and official evaluation have separate scopes.

Open questions

Assess the forced proofs and exact statement correspondence. The unforced alternatives A/B are separate unresolved targets; CMI’s evaluation is a distinct process.

Latest

CMI acknowledges the announcementSep 11, 2026
Pinned comparator proof revisionSep 10, 2026

Precise statement

Velocity u and pressure p satisfy $\partial_t u+(u\cdot\nabla)u=-\nabla p+\nu\Delta u+f$ and div u = 0, with viscosity ν > 0. The official question distinguishes whole-space ℝ³ from the periodic three-torus and unforced global regularity (A/B) from forced breakdown (C/D). Smooth, rapidly decaying data/force and uniformly bounded kinetic energy are required in the whole-space formulation.

Question paraphrased by OpenMath. Original wording is available in the sources.

Landscape

Figures and explorable examples. Selecting a statement opens its exact wording.

Where smoothness is guaranteed

A solution bounded in a norm on or below the scale-invariant line is smooth. Every weak solution is only known to be bounded on the higher line. The band between them is the gap: no general solution is known to have any norm there.

The gap between what is controlled and what is neededBounded here ⇒ smoothEvery weak solution is bounded hereL∞L³ endpoint

Controlling a norm at or below the line 2/p + 3/q = 1 gives smoothness.
The endpoint L∞L³: a bounded L³ norm rules out blowup.
Every Leray–Hopf weak solution controls the norms on 2/p + 3/q = 3/2.
Closing the gap for all smooth data would answer alternative (A).

Dataset navier-stokes-critical-scaling v1 · Exact rational exponent pairs (3/q, 2/p) on 2/p + 3/q = 1 for q ∈ {∞, 12, 6, 4, 10/3, 3} and on 2/p + 3/q = 3/2 for q ∈ {6, 5, 4, 3, 5/2, 2}; layers are the regions those statements describe. Software: python 3.12.13. Exact rationals, stored as floating point. SHA-256 0db7ec759c01… · Download JSON

Data

Layer	Status
Open: the gap between what is controlled and what is needed	open
Proved: bounded here ⇒ smooth (Ladyzhenskaya–Prodi–Serrin)	proved
Proved: every weak solution is bounded here (energy)	proved
Proved: L∞L³ endpoint (Escauriaza–Seregin–Šverák)	proved

Visual setup

The hypotheses change the fluid question

Transport and pressure are present in both fluid equations. Positive viscosity and external forcing distinguish the reported Navier–Stokes construction.

Reading boundary. Arrows describe terms and scope only. They are not measured forces, a numerical simulation or a visualization of the asserted singular flow.

Read the unforced whole-space targetQuestion scope Inspect forced whole-space breakdown◌ Proposed Inspect the forced periodic statement◌ Proposed

Use the selections to compare the exact forcing, domain and energy assumptions.

Text version

Four labeled contributions feed a velocity balance: transport, pressure, positive viscosity and an external force. A domain label separates whole space from the periodic three-torus. Selecting the unforced target highlights viscosity without activating the force; selecting forced results highlights both.

Three-dimensional incompressible flow; ν > 0. Schematic term relationships have no numerical scale.

Read the unforced whole-space target
Open
Unforced global regularity in the whole space
The official alternative A is not answered by the selected forced C/D constructions.
Unforced global regularity in the whole space →
Inspect forced whole-space breakdown
Proposed
Forced whole-space nonexistence
Theorem 1.1 and official alternative C. The manuscript and full formal endpoint are source-reported; mathematical assessment remains pending.
Forced whole-space nonexistence →
Inspect the forced periodic statement
Proposed
Forced breakdown on the three-torus
Corollary 10.6 and official alternative D; no unforced conclusion is asserted.
Forced breakdown on the three-torus →

Sources & review

Authored by OpenMath source curation on 2026-10-13 (AI-assisted curation). Independent review of this visual explanation is pending; linked assertions and relationships have their own assessments.

Navier–Stokes and Euler formal proof sourcesformalization.yaml; exact main declarations and Comparator instructionsProject documentationOriginal passage ↗
Existence and Smoothness of the Navier–Stokes EquationEquations (1)–(9) and alternatives (A)–(D)PublishedOriginal passage ↗
Navier–Stokes and Euler formal proof sourcesNavierStokes/ComparatorSolution.lean: navier_stokes_breakdown_periodicProject documentationOriginal passage ↗
Navier–Stokes and Euler formal proof sourcesNavierStokes/ComparatorSolution.lean: navier_stokes_breakdown_R3Project documentationOriginal passage ↗
Finite Time Blowup for Navier–StokesTheorem 1.1; Corollary 10.6; Section 1.1PreprintOriginal passage ↗

Results

The question 1

Open
Unforced global regularity in the whole space
The official alternative A is not answered by the selected forced C/D constructions.
Conjecture · Primary formulation
Open
Unforced global regularity in the whole space
For every ν > 0 and every smooth divergence-free initial velocity u₀ on ℝ³ whose spatial derivatives decay faster than every inverse power, the unforced incompressible Navier–Stokes equations admit global smooth velocity and pressure with uniformly bounded kinetic energy.
Assumptions
- Three space dimensions; whole-space domain ℝ³; viscosity ν > 0.
- No external force: f = 0.
- Every spatial derivative of u₀ is rapidly decreasing.
In this problem
The official alternative A is not answered by the selected forced C/D constructions.
Sources
- Existence and Smoothness of the Navier–Stokes Equation →
- Finite Time Blowup for Navier–Stokes →
Open statement page →

Proposed 3

Conditional implications 1

Proved
Unbounded compactly supported velocity prevents smooth continuation
A conditional consequence of continuity on a compact space-time set; it does not certify existence of a singular Navier–Stokes solution.
OpenAI 2026
Theorem · Conditional implication
ProvedOpenAI 2026
Unbounded compactly supported velocity prevents smooth continuation
If a smooth velocity field on ℝ³ × [0,T) is supported in one fixed compact spatial set and its spatial supremum norm has infinite limsup as t ↑ T < ∞, then it has no smooth continuation to ℝ³ × [0,∞) that agrees with it before T.
Assumptions
- The same compact set contains the velocity support for every time before T.
- Continuation must agree with the original velocity before the finite time T.
In this problem
A conditional consequence of continuity on a compact space-time set; it does not certify existence of a singular Navier–Stokes solution.
Sources
- Finite Time Blowup for Navier–Stokes →
Open statement page →

Variants and analogues 1

Open
Unforced global regularity on the three-torus
The official alternative B; a separate domain from whole-space regularity.
Conjecture · Different statement · related variant
Open
Unforced global regularity on the three-torus
For every ν > 0 and every smooth divergence-free periodic initial velocity, the unforced incompressible Navier–Stokes equations admit global smooth periodic velocity and pressure on ℝ³/ℤ³.
Assumptions
- Three-dimensional unit-periodic domain.
- Positive viscosity and no external force.
In this problem
The official alternative B; a separate domain from whole-space regularity.
Sources
- Existence and Smoothness of the Navier–Stokes Equation →
- Finite Time Blowup for Navier–Stokes →
Open statement page →

Connections

Consequences 1

Assuming A singular forced flow starting from restProposed

Finite energy alone does not ensure a smooth continuation
Conditional
If the reported compactly supported flow is valid, bounded kinetic energy can coexist with a velocity singularity that prevents a smooth continuation.
Limit This consequence is conditional on the reported singular flow and supplies no unforced example.
- Unbounded compactly supported velocity prevents smooth continuationProved
Sources & review
If a smooth velocity field on ℝ³ × [0,T) is supported in one fixed compact spatial set and its spatial supremum norm has infinite limsup as t ↑ T < ∞, then it has no smooth continuation to ℝ³ × [0,∞) that agrees with it before T.
A conditional consequence of continuity on a compact space-time set; it does not certify existence of a singular Navier–Stokes solution.
Assumptions & sources
- Finite Time Blowup for Navier–Stokes ↗Theorem 1.1; Corollary 10.6; Section 1.1
Source-grounded explanation · independent explanation review: pending.

Approaches

How the problem is attacked, and what each line of attack cannot yet reach.

Amplify localized oscillations while controlling the force

The manuscript builds a leading flow, high-order corrections and localized oscillations, then constructs smooth compact forcing and a whole-space breakdown example.

Cannot yet reach The PDE-term schematic explains the setup, not the analytic estimates of the proof.

Forced whole-space nonexistence (Proposed)
Forced breakdown on the three-torus (Proposed)

Sources & review

Supporting statements

Finite Time Blowup for Navier–Stokes ↗Theorem 1.1; Corollary 10.6; Section 1.1

Source-grounded explanation · independent explanation review: pending.

Timeline

Sep 11, 2026CMI acknowledges the announcementAssessment
The Institute states that evaluation will follow its deliberately unhurried process.
The announcement records no prize award or completed evaluation.
- Forced whole-space nonexistenceProposed
- Forced breakdown on the three-torusProposed
- Clay Mathematics Institute: Navier–Stokes announcement ↗Announcement dated 11 September 2026; evaluation process
Sep 10, 2026Pinned comparator proof revisionFormalization
The formal project exposes the exact C/D endpoints and self-assessed metadata.
This is a repository revision date, not a new discovery or an OpenMath execution.
- Forced whole-space nonexistenceProposed
- Forced breakdown on the three-torusProposed
- Navier–Stokes and Euler formal proof sources ↗formalization.yaml; exact main declarations and Comparator instructions
- Navier–Stokes and Euler formal proof sources ↗NavierStokes/ComparatorSolution.lean: navier_stokes_breakdown_R3
- Navier–Stokes and Euler formal proof sources ↗NavierStokes/ComparatorSolution.lean: navier_stokes_breakdown_periodic
Sep 8, 2026Manuscript and formal source releasedProposal
The public report gives a whole-space theorem and periodic corollary for every positive viscosity.
It uses external forcing and does not establish unforced viscous blowup.
- Forced whole-space nonexistenceProposed
- Forced breakdown on the three-torusProposed
- Finite Time Blowup for Navier–Stokes ↗Theorem 1.1; Corollary 10.6; Section 1.1
- On the Navier–Stokes Millennium Prize Problem ↗Our process; concurrent work; Euler and Navier–Stokes scope
Sep 5, 2026A forced breakdown argument is producedProposal
OpenAI’s later announcement dates its model-produced Navier–Stokes argument to 5 September.
This is a first-party account of discovery; public release and formal checking are later events.
- Forced whole-space nonexistenceProposed
- Forced breakdown on the three-torusProposed
- On the Navier–Stokes Millennium Prize Problem ↗Our process; concurrent work; Euler and Navier–Stokes scope
Also on the Frontier: Forced three-dimensional Navier–Stokes singularity
2000Four official existence/breakdown alternativesFoundation
Fefferman specifies decay, periodicity, forcing and energy hypotheses for the Millennium question.
The four alternatives must not be collapsed into one unqualified regularity assertion.
- Existence and Smoothness of the Navier–Stokes Equation ↗Equations (1)–(9) and alternatives (A)–(D)

Full history with sources →

Evidence

Evidence by kind
Literature	1 preprint · 2 projects Status OpenMath assessment · Oct 13, 2026. Proposed: Finite Time Blowup for Navier–Stokes · Forced whole-space breakdown reported ↗ · source dated Sep 8, 2026 · checked Oct 13, 2026Every positive viscosity; compact smooth force, zero initial velocity, bounded kinetic energy. Proposed: Navier–Stokes and Euler formal proof sources · Forced periodic breakdown reported ↗ · source dated Sep 8, 2026 · checked Oct 13, 2026Every positive viscosity; smooth periodic data and forcing.
Formal	2 complete proofs 2 formalizations below ↓ Reported in sources: Pinned Lean C/D nonexistence endpoints are reported complete, with zero sorry and standard logical axioms. They are distinguished from the manuscript’s stronger detailed singular-flow construction; OpenMath has not executed the project.
Computation	None recorded
Review	Not yet reviewed OpenMath assessment: OpenAI reports smooth forced breakdown in the whole space and on the three-torus, with full formal endpoints. The new arguments are under assessment; unforced regularity and official evaluation have separate scopes. Source comparison and reader curation; independent mathematical assessment remains pending. OpenMath pilot collection · OpenMath source curation · assessed Oct 13, 2026 · review due Jan 13, 2027 Collection last checked Oct 13, 2026.

Formalizations

Forced whole-space nonexistence →

Lean: forced whole-space breakdownComplete formal proof reported externally

Open formal source ↗

Complete formal proof reported externally

The endpoint matches official alternative C with explicit decay/force/energy predicates. The stronger from-rest compact singular-flow statement is separate and has no complete formalization asserted by this link. Metadata reports zero sorry and standard logical axioms only.

Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026

Declaration & revision

NavierStokes.Comparator.navier_stokes_breakdown_R3

Commit f9e8bc5b38b6e212696e8a30e3e91517af887bbd

Forced breakdown on the three-torus →

Lean: forced periodic breakdownComplete formal proof reported externally

Open formal source ↗

Complete formal proof reported externally

Exact periodic nonexistence endpoint for every positive viscosity. The comparator reference definitions and independent execution are separate checks; no unforced theorem is linked to this declaration.

Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026

Declaration & revision

NavierStokes.Comparator.navier_stokes_breakdown_periodic

Commit f9e8bc5b38b6e212696e8a30e3e91517af887bbd

External proof reports do not establish an OpenMath run, independent statement correspondence, or independent mathematical review.

Sources

Choose a starting point below. Each result links to its exact statement, cited passages and checks.

Start here

Introduction: Navier–Stokes existence and smoothness →

Bibliography 5

Existence and Smoothness of the Navier–Stokes Equation →
Charles L. Fefferman · Published · 2000
Equations (1)–(9) and alternatives (A)–(D)
Finite Time Blowup for Navier–Stokes →
OpenAI · Preprint · Sep 8, 2026
Theorem 1.1; Corollary 10.6; Section 1.1
Clay Mathematics Institute: Navier–Stokes announcement →
Clay Mathematics Institute · Project documentation · Sep 11, 2026
Announcement dated 11 September 2026; evaluation process
On the Navier–Stokes Millennium Prize Problem →
OpenAI · Project documentation · Sep 8, 2026
Our process; concurrent work; Euler and Navier–Stokes scope
Navier–Stokes and Euler formal proof sources →
OpenAI · Project documentation · Sep 8, 2026
formalization.yaml; exact main declarations and Comparator instructions

Research activity · 1 entry

Contributions

OpenAI is the printed manuscript author and credits an internal multi-agent research-model workflow for the mathematical argument. The announcement and formal metadata credit GPT-6 Astra/Codex for formalization. Fefferman and CMI own the official statement and evaluation process; Lean, Mathlib and Formal Conjectures/Comparator contributors support the proof infrastructure. Alpöge and Buckmaster’s separately credited forced-Euler work is not this Navier–Stokes theorem.

Formalization

Compare manuscript, comparator statement and proof dependencies

Check the official decay/periodic predicates, force regularity, energy condition and imported proof adapters at the pinned endpoints.

The inspected metadata is self-assessed; a local build and independent correspondence check are not attached.

Related statements · context, not additional proved progress

Existence and Smoothness of the Navier–Stokes Equation · sources & artifacts →

Navier–Stokes and Euler formal proof sources · sources & artifacts →

Selected literature; source observations and coverage limits are retained in the publication details.

Record details

Record version: 1
Classification: MSC2020 35Q30 / 76D03
Prerequisite level: specialist

Source observations & version history →

Overview

Current assessment

Open questions

Latest

Landscape

Where smoothness is guaranteed

The hypotheses change the fluid question

Unforced global regularity in the whole space

Forced whole-space nonexistence

Forced breakdown on the three-torus

Results

The question 1

Assumptions

In this problem

Sources

Proposed 3

Assumptions

In this problem

Formal proofs

Sources

Assumptions

In this problem

Sources

Assumptions

In this problem

Formal proofs

Sources

Conditional implications 1

Assumptions

In this problem

Sources

Variants and analogues 1

Assumptions

In this problem

Sources

Connections

Consequences 1

Related problems

Approaches

Amplify localized oscillations while controlling the force

Timeline

Evidence

Formalizations

Forced whole-space nonexistence →

Forced breakdown on the three-torus →

Sources

Start here

Bibliography 5

Contributions

Compare manuscript, comparator statement and proof dependencies