The part of Navier-Stokes no one is talking about

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 their conventional human-readable proof. Quite a few other mathematical conjectures have been settled recently using AI, and these have also been accompanied with formal proofs, using Lean 4 in particular. Until very recently, generating machine-verifiable formal proofs has been excruciatingly tedious. In 2005, Henk Barendregt and Freek Wiedijk wrote To give an indication of how much work is needed for formalisation, we estimate that it takes approximately one work-week (five work-days of eight work-hours) to formalise one page from an undergraduate mathematics textbook. That was the rule of thumb: forty hours per page. And this in the context of undergraduate…