> That's not a trivial if: stating the problem precisely is often as hard as the proof.

Really? You think 300 lines of Lean code [1] is just as hard as the proof (or even remotely close)? Also note, as the README says [2], that the theorem was written independently by formal conjectures, not by the LLM.

[1]:https://github.com/openai/NavierStokesAndEuler/blob/main/Com...

[2]: https://github.com/openai/NavierStokesAndEuler/blob/main/Com...