Equivalence of two Lean formalizations of the Navier–Stokes problem

This repository proves in Lean 4 that two independent formalizations of Fefferman's four statements (A)–(D) of the Clay Navier–Stokes problem state the same thing.

Purpose

OpenAI's Lean proof of Navier–Stokes breakdown (NavierStokesAndEuler) is checked with Comparator against challenge statements adapted from Google DeepMind's Formal Conjectures. A formal proof is only as good as its statement, so it matters whether that statement really says what Fefferman's (C) and (D) say.

As an independent cross-check, this repository proves that the original Formal Conjectures statements of all four alternatives are logically equivalent to the corresponding statements in a separately developed formalization, LeanDojo's LeanMillenniumPrizeProblems, which was written with different conventions (spacetime as ℝ⁴, coordinate partial derivatives, equations only for t > 0, …). Two independently written formalizations that are provably equivalent are much less likely to share a mistake than a single one is to contain one.

The Comparator challenge (NavierStokesAndEuler/ComparatorChallenges/NavierStokes.lean) differs from the original Formal Conjectures file only in its documentation, its namespace (NavierStokes.Comparator), local notation, the removed metadata attributes, and the omission of (A) and (B); its definitions and its statements of (C) and (D) are textually the same. Together with a successful Comparator run of OpenAI's proof, the equivalence therefore also means that the proof establishes LeanMillenniumPrizeProblems' FeffermanC and FeffermanD (this last combination is not carried out in this repository).

What this does not check: that either formalization matches the Clay problem text (the equivalence shows they agree with each other), and OpenAI's proof itself (that is Comparator's job).

The equivalence proof was generated by Claude (Anthropic), using Claude Code, and is checked entirely by Lean's kernel; no statement in it is assumed.

	Formal Conjectures	LeanMillenniumPrizeProblems
Copied from	google-deepmind/formal-conjectures FormalConjectures/Millenium/NavierStokes.lean (commit 8bf45ed)	lean-dojo/LeanMillenniumPrizeProblems Problems/NavierStokes/* and Problems/Common/Euclidean.lean (commit df469ba)
Location here	FormalConjectures/Millenium/NavierStokes.lean	Problems/
(A) existence on ℝ³	FormalConjectures.NavierStokes.navier_stokes_existence_and_smoothness_R3	MillenniumNavierStokes.FeffermanA
(B) existence on ℝ³/ℤ³	FormalConjectures.NavierStokes.navier_stokes_existence_and_smoothness_periodic	MillenniumNavierStokes.FeffermanB
(C) breakdown on ℝ³	FormalConjectures.NavierStokes.navier_stokes_breakdown_R3	MillenniumNavierStokes.FeffermanC
(D) breakdown on ℝ³/ℤ³	FormalConjectures.NavierStokes.navier_stokes_breakdown_periodic	MillenniumNavierStokes.FeffermanD

The LeanMillenniumPrizeProblems files are verbatim. The Formal Conjectures file has three changes, listed in its header:

• import FormalConjecturesUtil is replaced by import Mathlib and the two notations the file uses from Formal Conjectures' utility library (ℝ^n and ℝ³, scoped to EuclideanGeometry);
• the metadata attributes category and AMS are removed;
• the file is wrapped in namespace FormalConjectures (so NavierStokes.x becomes FormalConjectures.NavierStokes.x), because LeanMillenniumPrizeProblems also declares NavierStokes.divergence.

To see the complete diff:

curl -sL https://raw.githubusercontent.com/google-deepmind/formal-conjectures/8bf45ed70d48b2b2a501de9c00b26bfa38c573ee/FormalConjectures/Millenium/NavierStokes.lean \
  | diff - FormalConjectures/Millenium/NavierStokes.lean

Both are under the Apache License 2.0; see the LICENSE files in their directories.

Main results

In NavierStokesEquivalence/Main.lean:

theorem NSEquiv.existence_and_smoothness_R3_iff_feffermanA :
    (type_of% @FormalConjectures.NavierStokes.navier_stokes_existence_and_smoothness_R3) ↔
      MillenniumNavierStokes.FeffermanA
theorem NSEquiv.existence_and_smoothness_periodic_iff_feffermanB :
    (type_of% @FormalConjectures.NavierStokes.navier_stokes_existence_and_smoothness_periodic) ↔
      MillenniumNavierStokes.FeffermanB
theorem NSEquiv.breakdown_R3_iff_feffermanC :
    (type_of% @FormalConjectures.NavierStokes.navier_stokes_breakdown_R3) ↔
      MillenniumNavierStokes.FeffermanC
theorem NSEquiv.breakdown_periodic_iff_feffermanD :
    (type_of% @FormalConjectures.NavierStokes.navier_stokes_breakdown_periodic) ↔
      MillenniumNavierStokes.FeffermanD

(The left-hand sides are written out in full in the file, and checked by with_reducible rfl to be the types of the four Formal Conjectures theorems.) All four are proved viscosity by viscosity (existence_R3_at_iff, existence_periodic_at_iff, breakdown_R3_at_iff, breakdown_periodic_at_iff), from the equivalence of the conditions on the data and of the solution classes for given data (existsRn_iff, existsPeriodic_iff). None of the four statements is proved or assumed, and the proofs use only the standard axioms (propext, Classical.choice, Quot.sound); the sorrys in FormalConjectures/Millenium/NavierStokes.lean are the open-problem placeholders of Formal Conjectures and are not used.

What had to be proved

The two formalizations differ in several ways that are mathematically harmless but need proofs:

• Coordinates. Formal Conjectures fields are v : ℝ³ → ℝ → ℝ³ (smooth on ℝ³ × [0,∞)), LMPP fields are u : ℝ⁴ → ℝ³ with time as coordinate 0 (smooth on {t ≥ 0}). (Coordinates.lean)
• Where the equations hold. Formal Conjectures imposes the PDE and incompressibility on t ≥ 0 (one-sided time derivative, Mathlib's Laplacian, gradient, trace divergence); LMPP only on t > 0 with coordinate partial derivatives. Both are rewritten as within-derivatives on the closed half-space; the t = 0 case follows by continuity and density. (Solutions.lean)
• Decay conditions. Formal Conjectures bounds norms of all iteratedFDerivs with real exponents; LMPP bounds iterated coordinate partials, with the time derivatives of the force outermost and natural exponents, and bounds the force only for t > 0. This needs the multilinear comparison of the two kinds of derivative, the symmetry of higher derivatives of smooth functions (by induction on list permutations from Mathlib's second-order Schwarz theorem), and a density argument at t = 0. (Partials.lean, Data.lean)
• Energy and periodicity. MemLp versus HasFiniteIntegral, period-one versus integer-translation invariance. (Solutions.lean, Data.lean)
• Zero force. In (A) and (B) the force is 0 : ℝ³ → ℝ → ℝ³ in Formal Conjectures and fun _ => 0 : ℝ⁴ → ℝ³ in LMPP; these correspond under the change of coordinates, so (A) and (B) reduce to the same comparison of solution classes as (C) and (D). (Main.lean)

Building

Lean v4.34.0-rc2 and Mathlib v4.34.0-rc2 (the versions of NavierStokesAndEuler). With the project-local toolchain:

source /local/mirek/navier-stokes/toolchain/env.sh
lake exe cache get
lake build