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.
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.
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.
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 buildFor instructions on checking the formalizations with Comparator, see the ComparatorChallenges README.