Comment by QuesnayJr
19 hours ago
Someone has to actually check this. I'm guessing OpenAI had someone check it internally, but it's possible to get it wrong.
19 hours ago
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...