Navier-Stokes and Lean

This blog post discusses the relationship between the Lean proof assistant and recent advancements in AI, particularly in regard to the Navier-Stokes equations, a Millennium problem. It draws insights from Kevin Hartnett's book 'The Proof in the Code' and highlights significant mathematical projects utilizing Lean. The author reflects on the evolving use of Lean in formal proofs and how AI now assists in generating proofs, shifting the landscape of mathematical publication.