The construction is that there is one file you need read and verify, the challenge file. If you've verified that file and trust that your lean compiler works correctly, the proof will be correct.

That file should be https://github.com/openai/NavierStokesAndEuler/blob/main/Com... in this case (286 lines).

Had no idea this was what lean looked like- that's mind blowing. I'm not even sure how someone would critique this if they wanted to