Yesterday OpenAI announced a proof settling a long-standing question about the Navier-Stokes equations. But an overlooked aspect: they also posted a Lean 4 formal proof alongside the human-readable one.

Until recently, formal proofs were tedious. In 2005, Henk Barendregt and Freek Wiedijk estimated one work-week to formalize one page of an undergraduate math textbook. Research papers are denser. Formalizing OpenAI's 166-page paper might take 132,800 person-hours. OpenAI verified their proof in Lean in 17 hours.

Lowering the cost by four orders of magnitude is revolutionary. I've used AI to generate formal proofs for a blog post; I wouldn't dream of doing that if it cost a week's salary.

Formal verification applies beyond math: security policies, smart contracts, mission-critical algorithms. These are easier and have clearer ROI.