The "statements" here are statements of lemmas, not the statement of the main theorem. The main theorem statement was written by humans (prior to the OpenAI work), so there shouldn't be any concern that an AI mistranslated it.

That could be that these examples are lemmas, but in the introduction the authors conclude,

"In all cases the correctness of the formal proof does not say anything about the correctness of the NL proof."

The Clay Mathematics Institute has not yet accepted the proof as it takes a while to review.

"The Clay Mathematics Institute is dedicated to furthering the beauty, power and universality of mathematical thought. Curating the Millennium Prize Problems is one of the most important ways in which it pursues this goal. The rules governing the prizes describe the process for evaluating what has been achieved and for assigning credit. The process is deliberately unhurried, but we will provide updates."

https://www.claymath.org/news/navier-stokes-announcement/

We can see therefore that we don't know if the OpenAI program wrote the NL statement or proof correctly. Or if maybe it needs work. Or if maybe it has significant errors.

We also don't know if Astra properly wrote the initial statement of Navier-Stokes correctly in Lean.

My point is that Astra did not write the statement of Navier-Stokes in Lean, there was already a human-written statement, so there should be no concern that it has errors.

This article shows that we can't conclude from the working Lean proof that the NL proof is also correct, because they are different in some places. On the other hand I think it's unlikely that it's "very" broken. OpenAI first spent a lot of computer time to find the NL proof, and then less time to translate it into Lean. So if there were errors in the NL proof it seems they were not fatal, the agent translating it into Lean was able to patch them up as it went along.