John D. Cook flags a detail he says the coverage of OpenAI’s Navier-Stokes announcement skipped: alongside the human-readable proof, OpenAI published a Lean 4 formal proof. Lean is a proof assistant — software that checks a proof step by step, so “verified” means a machine confirmed the reasoning, not that a reviewer found it persuasive.

That combination — AI generating the proof, a checker certifying it — is becoming standard for AI-assisted mathematics. What makes it notable is the price.

  • In 2005, mathematicians Barendregt and Wiedijk estimated roughly one work-week (about 40 hours) to formalize a single page of an undergraduate textbook.
  • Research papers are denser and their dependencies wander across the whole literature, so Cook assumes a 20x multiplier for them.
  • On that basis, hand-formalizing OpenAI’s 166-page paper would run to roughly 132,800 person-hours.
  • OpenAI verified its proof in Lean in 17 hours. A commenter estimates the compute at $1–2 million — still cheaper than the human route by roughly an order of magnitude.

Cook is careful with the word “revolutionary.” But lowering the cost of machine-checked reasoning by four orders of magnitude changes who can afford it. He now generates formal proofs just to check his own blog-post math — something he says he would never have done when it cost a week of someone’s salary.

The applications he points at are less glamorous than fluid dynamics and more straightforwardly useful: proving that a set of security policies is internally consistent, that a smart contract caps liability at a stated amount, that a mission-critical algorithm does what its spec says. Those are easier to formalize than research mathematics, and their return is easier to price.

The comment thread supplies the honest caveats. Verification confirms you built what you specified — it says nothing about whether you specified the right thing, and that gap stays human and stays expensive. What does change is review: a proof becomes a checked artifact you can diff and point at, instead of a prose argument each new reader has to reconstruct.

One commenter argues the real achievement is the coordination tooling that let agents track which subgoals had actually been proved — infrastructure, not model. And the underlying announcement has itself been contested by mathematicians, so treat the result as an open question. Cook’s subject is the machinery that checks it.