Navier-Stokes and Lean

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. And then yesterday OpenAI announced a 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 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 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…