On: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

[maths_math]

What would be the point of that though? I think the reason Kevin wants to optimize it is for the understanding that will result from the process, not because anyone cares about having a Lean proof that compiles quickly...

[andrewchambers → maths_math]

I was replying to the comment about it being slow to run. I wasn't commenting on understanding it.

[jchanimal → maths_math]

Then run the annealer and learn from the result.