2 ms·
Someone has to actually check this. I'm guessing OpenAI had someone check it internally, but it's possible to get it wrong.
by QuesnayJr 25d ago
Someone has to actually check this. I'm guessing OpenAI had someone check it internally, but it's possible to get it wrong.
- Aaron1011 25d agoIn 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/8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538/ComparatorChallenges/NavierStokes.lean#L26 https://github.com/openai/NavierStokesAndEuler/blob/8937a8f4...