OpenAI's Navier-Stokes proof shipped with a Lean 4 formalization verified in 17 hours

Earlier this week, OpenAI announced a proof that it says settles a long-standing question about the Navier-Stokes equations, the partial differential equations that govern fluid flow. The claim generated immediate buzz. But writing on his blog, John D. Cook argues that the announcement's most consequential detail is going almost entirely unremarked: alongside its conventional, human-readable paper, OpenAI simultaneously published a formal proof of the result in Lean 4, the proof assistant that mechanically checks every step of an argument.

The overlooked detail

According to Cook, whose post surfaced on the Hacker News front page, OpenAI released a 166-page paper and a Lean 4 formalization of the proof at the same time. Nor, he notes, is this an isolated gesture: several recent mathematical conjectures settled with AI assistance have likewise been accompanied by formal proofs, Lean 4 in particular.

Formalization used to cost a week per page

To explain why that matters, Cook reaches back to a 2005 estimate by Henk Barendregt and Freek Wiedijk: formalizing a single page of an undergraduate mathematics textbook took roughly one work-week, about forty hours. And that was for textbooks, where page 100 depends mostly on pages 1 through 99. A sentence in a research article can cite anything ever published before it, so the density, and therefore the effort, is far higher.

Cook's back-of-envelope calculation runs as follows. Assume a research paper page is twenty times harder to formalize than a textbook page. OpenAI's 166-page paper would then have cost around 132,800 person-hours to formalize by hand. Instead, OpenAI's Lean verification of the proof took 17 hours. Cook writes that he hesitates to use the word, but lowering the cost of anything by four orders of magnitude is revolutionary. The 132,800 figure is an extrapolation from a 2005 rule of thumb rather than a measured benchmark, but even with a generous margin of error, the gap is dramatic.

Cook adds that he has already used AI to generate formal proofs to check his own work for a blog post, something he would never consider if it meant paying someone a week's salary for the check.

Verification beyond mathematics

Formal verification is not confined to pure mathematics, Cook points out. Among the applications he lists: proving that a set of security policies is internally consistent and, under stated assumptions, actually accomplishes its purpose; proving that a smart contract imposes a specified maximum liability; and verifying the correctness of mission-critical algorithms. These problems, he argues, are easier than formalizing research mathematics, and the return on investment is easier to quantify.

Why it matters

The Navier-Stokes result is a major research event in its own right, but the durable news may be the economics around it. If AI can now produce formal proofs at a cost orders of magnitude below manual formalization, machine verification stops being a luxury reserved for textbook exercises and becomes a practical default.

For AI-assisted mathematics specifically, that changes the trust question. A Lean-checked proof does not need to be taken on faith from a model or from its authors, because the proof assistant validates every step. And if AI-settled conjectures now routinely ship with Lean 4 formalizations, as Cook observes they have begun to, machine verification may become the expected standard for accepting major results.

For software engineering, the same collapse in cost has more immediate payoffs. Security policies, smart contracts and mission-critical algorithms are, by Cook's account, easier targets than research mathematics, which suggests formal methods could move from exotic to routine exactly where mistakes are most expensive.