Those are statements about auto-formalization and the NL proof. They're saying that further work needs to be done on verifying whether the Lean and NL proofs are equivalent, which is completely valid. But they're not disputing that the Lean formalization is a correct statement of the Millennium Prize problem. You can see in the link I provided (and the original pull request) that it was written by humans, reviewed by human experts, and is completely independent of the OpenAI effort.
"3.1. When the NL paper declares stronger statements than what Lean proves
We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement."
It seems the Lean version may not be a correct statement of the Navier-Stokes problem.
They go on to say this--
Remark 3.4 (Further potential mistranslations of the Navier-Stokes proof). The above examples require careful manual checking of both the NL proof as well as the Lean proof, which is delicate and highly time consuming. Moreover, the fact that we display only two examples does not mean that these are the only cases of mistranslations.