Navier-Stokes and Lean

OpenAI announced a solution to the Navier-Stokes Millennium Prize problem, fully formulating its results in the Lean proof assistant, according to a post by the company. Hours earlier, Tristan Buckmaster posted about separate progress with Levent Alpöge, saying they have Lean-verified proofs for three public results but held back a "blowup for hypo-dissipative Navier Stokes" because Lean verification had not finished. Lean, first developed by Leonardo de Moura in 2013 as a Microsoft project for proving code correct, is now being used as a time-stamp to claim theorems before they are written up.

I was working on this week's post on Lean after reading Kevin Hartnett's book The Proof in the Code: How a Truth Machine Is Transforming Math and AI https://www.amazon.com/Proof-Code-Truth-Machine-Transforming/dp/0374620059?&linkCode=ll2&tag=computation09-20&linkId=4743d071611d851dd46c9ffdee796f51&language=en US&gaOptInStatus=true&ref =as li ss tl . And then yesterday OpenAI announced a solution https://openai.com/index/navier-stokes-solution/ to Navier-Stokes, one of the Millennium problems. An incredible accomplishment to say the least. Hours earlier Tristan Buckmaster posted about his progress with Levent Alpöge https://cims.nyu.edu/~tristanb/statement.pdf based on a program started by Diego Córdoba and Luis Martínez-Zoroa, and his interactions with OpenAI. I'm still trying to understand what happened and will write more later but I recommend the Quanta article https://www.quantamagazine.org/ai-has-solved-one-of-maths-1-million-millennium-prize-problems-20260908/ to get you up to speed. Lean plays a major role for both projects. OpenAI fully formulated their results in Lean. Buckmaster said they have Lean-verified proofs for the three results they made public but held back on the "blowup for hypo-dissipative Navier Stokes" because the Lean verification has not finished. So it's worth taking a look back. Leonardo de Moura developed the first version of Lean in 2013 as a Microsoft project for proving code correct. Hartnett tells the story of the people involved in the development of the various versions of Lean capturing the excitements and disagreements. What caught me was the lack of backward compatibility, the definitions and theorems formalized in one version of Lean might break in the next. There was a constant need to get the libraries back up to date until the development stabilized. The best part of the book focused on some big projects in Lean. And now Lean, particularly in the Navier-Stokes papers, is being used as a time-stamp, a way to claim your theorem before having to write it up properly in an explainable way. Buckmaster even held back a result because it wasn't yet Lean verified. The way we even publish results is a-changing.