Someone has to actually check this. I'm guessing OpenAI had someone check it internally, but it's possible to get it wrong.

In this case, there was already an existing Lean statement of the problem in the formal-conjectures repository, which they re-used: https://github.com/openai/NavierStokesAndEuler/blob/8937a8f4...