The part of Navier-Stokes no one is talking about

OpenAI announced a proof that settled a long-standing question about the Navier-Stokes equations from fluid dynamics, and simultaneously posted a Lean 4 formal proof of the result. The formal proof aspect has received little attention compared to the announcement itself.

Yesterday OpenAI announced a proof that settled a long-standing question about the Navier-Stokes equations from fluid dynamics. The announcement has created a lot of buzz, as one would expect. But there’s an aspect of OpenAI’s work that I haven’t seen anyone talk about: they posted a Lean 4 formal proof at the same time as … The post