The part of Navier-Stokes no one is talking about
OpenAI's recent proof of the Navier-Stokes equations is notable not just for the mathematical breakthrough, but for the inclusion of a machine-verifiable formal proof in Lean 4. This development suggests a massive reduction in the cost and time required to verify complex mathematical research.
Why it matters
The ability to automate formal verification could revolutionize scientific research and software security by making rigorous proof-checking exponentially faster.
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.
Get smarter about the news
Sign up free for a feed built around what you actually care about, Dive Deeper research on any story, and the full text of every article.
Create free accountAlready have an account? Sign in