Navier-Stokes Proof Notes
In-progress notes on a geometric approach and Lean 4 formalization
These notes are not yet ready for publication.
Like a smooth solution to the Navier-Stokes equations,
we can't yet prove this exists for all time.
In the meantime, explore existing approaches or learn why the problem is so hard.
Check back soon — we're closing in on the last few sorrys.
$$\text{Proof} \in L^\infty_t(\texttt{navier-stokes.org})$$
remains an open conjecture.
We have existence but not yet regularity of this page.
The solution is known to blow up in a finite number of sorry leaves.
$\square$ will appear here when $\texttt{lake build}$ returns $0$ axioms on the CMI path.