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.