Formal Verification of 2D Navier-Stokes Nonlinear Energy Conservation in Lean 4 (v3: complete package)

Zenodo (CERN European Organization for Nuclear Research) 2026 Preprint Open access

Read full text
Authors: Navin Dutta, Profiled AI Research
DOI: 10.5281/zenodo.18853534
Cited by: 0

Abstract

0-sorry Lean 4 proof: nonlinear term vanishes for 2D incompressible flow. Uses Mathlib IBP. NOT the Millennium Prize.

Fields of Study & Subjects

Navier-Stokes equation solutions Logic programming and type systems Computational Fluid Dynamics and Aerodynamics

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
3 March 2026
Language
EN
Document type
Preprint