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

[Ohentis]

I mean they might not have tried spending 30 million dollars with a new model yet.