John D. Cook reads OpenAI's Navier-Stokes release as a formal-methods result, not only a mathematics one

Sources: primary, discussion
Summary: John D. Cook argues OpenAI's Navier-Stokes announcement matters as much for machine-checked proof as for the mathematics, because the 166-page paper shipped a Lean 4 formal proof alongside the human-readable one. He reports Lean verified that proof in 17 hours. He contrasts that against his own extrapolation of roughly 132,800 person-hours, derived from a 2005 rule of thumb of forty hours per textbook page and an assumed 20x multiplier for research density.
Why it matters: If machine-checked proof is getting cheap at this rate, the same tooling comes within reach of security policy consistency and mission-critical algorithm correctness.