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 co

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/ComparatorChallenges/NavierStokes.lean https://github.com/openai/NavierStokesAndEuler/blob/main/Com... in this case (286 lines).