Comment by lovasoa

If I understand well, they mean that the thing they proved in lean is not Navier Stokes. And they don't make any statement about whether the natural language proof is correct or not.