Navier Stokes misformalization

[mirefek]

As discussed on Zulip, and demonstrated in Lean, there are some mistakes in the current formalization of Navier Stokes. It should be made clear in README that the state of Navier Stokes is not yet ready to be used as the golden target for solution attempts, and more Lean & PDE experts should look into it.

[mirefek]

There is now an alternative formalization in the review process for formal_conjectures:
google-deepmind/formal-conjectures#1457

[Robertboy18]

Thanks for flagging this (and for the Lean repo link, you can keep your formal conjectures one in the deepmind repo as it is!). We agree the previous Navier–Stokes formalization on main was not a fully faithful encoding of Fefferman’s Clay statement and could be satisfied vacuously (e.g. by choosing a degenerate domain), so it should not have been presented as a “golden target”. I did however engage in discussions on zulip and fixed some issues.

We have now updated main to fix this properly:

Clay-aligned statement (Fefferman A–D).

• The Navier–Stokes Millennium problem statement is now a direct formalization of Fefferman’s Clay PDF (navierstokes.pdf), split by domain:
• MillenniumRDomain.lean: conditions (4)–(7) and statements (A),(C)
• MillenniumBoundedDomain.lean: conditions (8)–(11) and statements (B),(D) + combined disjunction
• single entry point: Millennium.lean exporting MillenniumNavierStokes.NavierStokesMillenniumProblem

Closed the “vacuous domain” loophole.

• We refactored the core PDE scaffold in Navierstokes.lean so the relevant spacetime domain is derived from the time horizon (TimeDomain n T) rather than being an arbitrary field that can be set to ∅. This prevents the earlier style of vacuity exploit.

README updated accordingly.

• The README.md status section now describes Navier–Stokes as a direct Clay translation, and the per-problem details explain what’s formalized (the statement) vs what remains external (the analytic theory/proof).

Some notable differences compared to your PR #1457 - our encoding is more “coordinate-explicit”: we model spacetime as Euc ℝ (n+1) and express the PDE via iterated coordinate partials (partialDeriv / iteratedPartialDeriv) to mirror the PDF’s ∂_x^α ∂_t^m style. Your PR is more “mathlib-native”: v : ℝ^n → ℝ → ℝ^n with deriv in time and fderiv/iteratedFDeriv in space, and smoothness via ContDiffOn on univ ×ˢ Ici 0. One semantic difference to flag: your PDE clause is stated for t > 0, whereas we require it on t ≥ 0, and in the periodic setting you require periodicity of both velocity and pressure, while the Clay text explicitly requires periodicity for u (condition (10)) but doesn’t separately assert it for p.

If you’d like to align the two statements, the most concrete reconciliation points seem to be: (1) decide whether the PDE should be required for t ≥ 0 or t > 0 (and how that interacts with the initial condition and ContDiffOn), and (2) decide whether to keep pressure periodicity as an explicit hypothesis or make it derived/optional to match the PDF literally. We’d be happy to cross-review and sync terminology/strength so readers can easily see they’re the “same” Clay statement (modulo routine formalization choices).

[mirefek]

Thanks for the response, I might give it a look later. Just to comment on your comparison

• Periodicity of p is stated in errata in the document by Clay Institute (page 6).
• We think that stating the condition for t > 0 while having smoothness on t >= 0 forces the condition to hold the right way even on the boundary. However whether to force it only for t > 0, or to make it more explicit, and take care of one-sided derivatives, is discussed in the thread about the PR (it can get changed).

[Robertboy18]

Thanks for the suggestion! I added the periodicity of p! That makes sense for your other point.