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.

• Read the blog post
• Read the Navier-Stokes paper
• Read the Euler paper

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.