NavierStokesAndEuler: Navier-Stokes Finite Time Blowup, Mathematically Proven and Verified in Lean 4

This repository formalizes the finite time blowup phenomenon of the Navier-Stokes equations, one of the Clay Mathematics Institute's Millennium Prize Problems, in Lean 4. It implements the mathematical results proposed by OpenAI as Lean 4 code, which is mechanically verifiable, thereby eliminating the possibility of logical errors.

It proves that no global smooth solutions exist when the viscosity coefficient is positive in the whole space R^3 and the periodic torus R^3/Z^3. For the incompressible Euler equations, it includes the process by which an initial velocity field that is smooth and has compact support in R^3 forms a singularity in finite time.

It supports independent proof verification using Mathlib and the Lake build system. It provides a case study of computers directly verifying complex fluid dynamics theory for researchers who prioritize mathematical rigor or developers interested in formal proofs.