Lean 4.34.0-rc2 checks proofs, not fluid simulations
NavierStokesAndEuler contains formal certificates for results in two OpenAI papers. The Navier-Stokes development states finite-time breakdown results for smooth forced flow on three-dimensional Euclidean space and the periodic torus, for every positive viscosity. The Euler development states an unforced singularity result from smooth, compactly supported, divergence-free initial velocity. Nothing here advances a numerical time step, draws a vortex, or helps an engineer model airflow. The output is accepted theorem declarations inside Lean.
That distinction matters because the repository is easiest to misuse as a headline prop. A kernel-checked proof can establish that declarations follow from definitions and permitted axioms. It does not by itself establish that the formal definitions perfectly capture every intended sentence in a paper, or that the wider mathematical community has accepted the argument. OpenAI's metadata maps four main declarations to the source papers and labels the repository's review status as self-assessed.
Four main declarations report zero proof placeholders
The formalization.yaml file identifies 4 main results: two Navier-Stokes breakdown declarations and two Euler declarations, including a finite maximal-lifespan singularity statement. It reports sorry_count: 0 for each and names three permitted axioms: propositional extensionality, classical choice, and quotient soundness. Those are project metadata claims we read from the repository; our lab did not independently ask Lean to confirm them.
The Comparator challenge files deliberately contain sorry placeholders because they define the problems a submitted solution must fill. Their comments say the reference statement does not sit in the proof root or submission imports. Separate JSON configurations point Comparator at the solution modules, enumerate the theorem names, permit the same 3 axioms, and enable the Nanoda checker. This separation is more useful than merely saying the main tree is complete because it gives a reviewer an isolated target.
What happened when we ran it
There is no executed lab result for commit f9e8bc5. Our harness did not support the Lean ecosystem, and the repository had no Dockerfile that could supply its own environment. We therefore have no measured installation time, build outcome, test count, dependency footprint, or vulnerability scan. Any claim that the formalizations compile in our sandbox would be false.
The absence of a run is a limitation of this review, not evidence against the proof. It also means the repository's central promise remains unchecked by our usual fresh-container method. For this project, the next useful verification is specific: install the pinned Lean release candidate, fetch the matching Mathlib cache, run the full Lake build, then execute both Comparator challenges with the external checker tools present.
Independent checking needs three tools beyond Lake
The basic path pins Lean 4.34.0-rc2 and Mathlib at v4.34.0-rc2. With elan installed, the README gives two commands: lake exe cache get and lake build. The Lake file defines NavierStokes, Euler, and ComparatorChallenges as default targets, and it pulls Comparator at the same release candidate. Apache-2.0 covers the repository, which is straightforward for research reuse and redistribution.
Comparator adds landrun, lean4export, and nanoda_bin to the setup. Reviewers then run one challenge command for Navier-Stokes and another for Euler. This is a better fit for an independent audit than importing the solution into its own theorem statement and accepting a normal project build. It still does not review the correspondence between the original prose argument and every Lean definition. A PDE expert and a formalization expert have different work to do.
Two commits provide a snapshot rather than a project history
The repository was created on September 8, 2026, received its second and latest commit on September 10, and had no GitHub releases. GitHub showed 2,016 stars, 207 forks, and 0 open issues or pull requests on October 1. The attention is unsurprising given the claimed result. Zero issues in a two-commit repository should not be read as defect evidence or proof that outside review has concluded.
The linked OpenAI post says the organization does not intend to claim the Millennium Prize for the result. That restraint belongs in the adoption judgment. NavierStokesAndEuler is the right artifact for checking what was formalized and how the declarations connect to the papers. It is the wrong artifact for learning fluid dynamics from scratch, running CFD, or outsourcing mathematical judgment to a green badge. The repository also gives reviewers a precise map from paper results to Lean declarations, which is more useful than a generic claim of formal verification. Start with the paper, compare those four mappings, then use Lean and Comparator to test the exact formal claim. Record the pinned tool versions and checker outputs so another reviewer can reproduce the same assessment.