What is this?
This repository contains Lean 4 formalizations (machine-checked formal proofs) of two OpenAI papers: 'Finite time blowup for Navier-Stokes' and 'Finite time blowup for the Euler equation'.
This repository contains Lean 4 formalizations (machine-checked formal proofs) of two OpenAI papers: 'Finite time blowup for Navier-Stokes' and 'Finite time blowup for the Euler equation'.Is this a reusable code library or a set of formal math proofs?It is a collection of Lean 4 / Mathlib proof scripts tied to specific published results, not a general-purpose software library you would import into other projects.
It is a collection of Lean 4 / Mathlib proof scripts tied to specific published results, not a general-purpose software library you would import into other projects.How do I build and check these formalizations?Install elan, fetch the Mathlib cache, and then build the project with Lake.
Install elan, fetch the Mathlib cache, and then build the project with Lake.What tools do I need before building this?You need Lean 4.34.0-rc2, Mathlib, and Lake, managed through the elan toolchain installer.
You need Lean 4.34.0-rc2, Mathlib, and Lake, managed through the elan toolchain installer.Does this fully solve the Clay Navier-Stokes Millennium Prize Problem?No. It formalizes two specific 'breakdown' alternatives (C and D) from the Clay Mathematics Institute's official problem description, not a general proof or disproof of the full existence-and-smoothness statement.
No. It formalizes two specific 'breakdown' alternatives (C and D) from the Clay Mathematics Institute's official problem description, not a general proof or disproof of the full existence-and-smoothness statement.Who is this repository meant for?It is aimed at mathematicians and Lean/Mathlib users who want to independently verify OpenAI's blowup proofs, not at general software developers.
It is aimed at mathematicians and Lean/Mathlib users who want to independently verify OpenAI's blowup proofs, not at general software developers.What exactly does the Euler result prove?It constructs smooth, compactly supported, divergence-free initial velocity on R3 whose solution to the unforced incompressible Euler equations develops a singularity in finite time, with the velocity's C1 norm becoming unbounded and the vorticity's L-infinity norm diverging in time.
It constructs smooth, compactly supported, divergence-free initial velocity on R3 whose solution to the unforced incompressible Euler equations develops a singularity in finite time, with the velocity's C1 norm becoming unbounded and the vorticity's L-infinity norm diverging in time.What is Comparator used for here?Comparator is an independent tool for checking the correctness of the Lean formalizations; instructions for using it are documented in the ComparatorChallenges README.
Comparator is an independent tool for checking the correctness of the Lean formalizations; instructions for using it are documented in the ComparatorChallenges README.Does the Navier-Stokes result need viscosity or a special domain?The results hold for every positive viscosity and are proven separately for the whole space R3 and for the periodic torus R3/Z3, each with specially constructed smooth initial data and forcing.
The results hold for every positive viscosity and are proven separately for the whole space R3 and for the periodic torus R3/Z3, each with specially constructed smooth initial data and forcing.Can I just read this to learn Lean or Mathlib?It's possible but not ideal as a tutorial; it's a dense, research-grade formalization of advanced PDE results rather than an introductory Lean/Mathlib resource.
It's possible but not ideal as a tutorial; it's a dense, research-grade formalization of advanced PDE results rather than an introductory Lean/Mathlib resource.What are similar projects?math, fermats-last-theorem, fluid_lean, integer-mult-bounds, sympy, open-ontologies, Choir, NSNFSSSFSFN
math, fermats-last-theorem, fluid_lean, integer-mult-bounds, sympy, open-ontologies, Choir, NSNFSSSFSFNWhich topics is it in?lean, theorem-proving, verification, research-tools, science, physics, math, functional-programming, mathematics, paper, academic, academic-research
lean, theorem-proving, verification, research-tools, science, physics, math, functional-programming, mathematics, paper, academic, academic-research