3 ms·
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/Na
by Aaron1011 25d ago
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/8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538/ComparatorChallenges/NavierStokes.lean#L26 https://github.com/openai/NavierStokesAndEuler/blob/8937a8f4...