Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs