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 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.

• Tom Hales wanting to convince the world that his proof of the Kepler Conjecture was correct.
• Peter Scholze wanting to convince himself of the correctness of his liquid tensor experiment.
• Kevin Buzzard, Johan Commelin and Patrick Massot formalizing Scholze's Perfectoid Spaces to show Lean can handle modern mathematical objects.
• Terence Tao wanting to formalize in Lean the proof with Tim Gowers, Ben Green and Freddie Manners of the polynomial Freiman-Ruzsa conjecture, just to show it could be done.

None of these were individual efforts but required teams of volunteers to fill in details. Tao approached his proof as a polymath project and his superstar status in the math community really helped get volunteers and popularized Lean.

I did learn a new term from the book, the "de Bruijn factor", the ratio of the length of the formal computer proof to the length of the human proof. I suspect the factor is very large for proofs in theoretical computer science, particularly computational complexity which is why we haven't seen many computer science theorems formalized in Lean.

Hartnett's story ends at the January 2025 Joint Math Meetings in Seattle, a conference I attended. He talks about the initial connections between AI and Lean, but not the uncertain AI future that started to worry mathematicians. By the time the book was published in June 2026, we had seen tremendous progress in AI proving theorems. We've seen even more progress in the three months since, even in the last three days given the news above.

Lean plays a different role now. No longer do you need to write Lean code, any more than you need to write Python code, you can just use AI to generate it. Anthropic fully formalized Fermat's Last Theorem in Lean just last week and hardly caused a stir. 

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.