You're correct that nobody really understands what these huge Lean proofs actually say. However, the initial statement, even for Navier-Stokes, is not very long [0]. Still, you are also right that sometimes the problem statement can be wrong but it is highly unlikely here.

[0] https://github.com/openai/NavierStokesAndEuler/blob/main/Com...