Finite time blowup for Navier–Stokes and Euler equations

This repository contains Lean 4 formalizations of the results presented in “Finite time blowup for Navier–Stokes” and “Finite time blowup for the Euler equation” by OpenAI.

Navier Stokes

For every positive viscosity, we prove two results:

• Whole space $\mathbb{R}^3$: There exist smooth initial data and forcing for which no global smooth solution with uniformly bounded kinetic energy exists.
• Periodic torus $\mathbb{R}^3/\mathbb{Z}^3$: There exist smooth periodic initial data and forcing for which no global smooth solution exists.

These are alternatives (C) “Breakdown of Navier–Stokes solutions on ℝ³” and (D) “Breakdown of Navier–Stokes Solutions on ℝ³/ℤ³” in the Clay Mathematics Institute’s official problem description of the Navier–Stokes existence and smoothness Millennium Prize Problem.

Euler

We construct smooth, compactly supported, divergence-free initial velocity on $\mathbb{R}^3$ whose solution to the unforced incompressible Euler equations develops a singularity in finite time. The velocity’s $C^1$ norm becomes unbounded near that time, and the time integral of the vorticity’s $L^\infty$ norm diverges.

Building the formalizations

The project uses Lean 4.34.0-rc2, Mathlib, and Lake. With elan installed, fetch the mathlib cache and build the formalizations with:

lake exe cache get
lake build

Independent proof checking

For instructions on checking the formalizations with Comparator, see the ComparatorChallenges README.