And yet I cited a specific statement made concerning N-S specifically, whereas all you’ve done is make patronizing remarks, and strawman arguments.
Have you actually read it? They give a handful of examples of mistranslations of both claims and proofs thereof, in relation to NS and Euler, though I do concede that they do not go as far as claiming outright the NS statement itself is mistranslated.
Unfortunately, lean proof alone is not enough. sidestepping the raging discussion regarding the meaning of mathematics, just because the lean compiles is not proof in itself that it is correct in the sense that mathematicians mean. Unless of course, you can prove that lean itself is correct, which you can’t.
we have seen “proofs” earlier this year that essentially abused some bugs in the kernel. it would be very convenient if every program written in rust was automatically correct if compiles - something i strongly suspect you believe - unfortunately, this is not the case for either.