>No one is disputing that the Lean formaization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.

These authors don't seem to be disputing that this Lean formalization of Navier-Stokes is correct. I don't think that gives us any new information about whether the generated Lean proof is or isn't a valid proof of this N-S blowup thing.