Machine-verified conditional proof of 3D Navier-Stokes regularity in Lean 4 with 175+ theorems and zero sorry. Reduces the Millennium Prize problem to a single axiom: barrier growth with enstrophy. Three independent arguments for the remaining axiom supported by DNS evidence (P(β>0)=97.8%).
Anthony W. Eckert (Sat,) studied this question.