Audit published
Finite time blowup for Navier–Stokes
Curated listing · PDF
Lean formalisations (2)
Choose a formalisation to inspect its evidence.
openai/NavierStokesAndEuler at f9e8bc5b38b6
Linked by the repository’s formalization.yaml.
Project review: self-assessed
Audit: awaiting publication.
cgarryZA/NavierStokesAndEuler at e06440b7d441
Linked by the repository’s formalization.yaml.
Project review: self-assessed
- Open the audit by Christian Garry — Links 77 of the paper's 79 numbered statements, each with a coverage reading (full, composed, partial or changed), and records statement reviews of Lemmas 8.6 and 10.5.
Related
- Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs — Alexander Bastounis, Fabian Circelli, Anders C. Hansen. A paper on how this paper's statements correspond to the Lean formalisation.