Presents a machine-verified conditional proof of Navier-Stokes regularity in Lean 4 with 175+ theorems and 0 sorry. The proof reduces the Millennium Prize problem to a single irreducible axiom: the existence of positive barrier growth parameters (a, β > 0) such that the Kramers barrier grows as any positive power of enstrophy. All other steps are either machine-verified or cite published PDE results with properly-typed signatures.
Anthony W. Eckert (Sat,) studied this question.