OpenAI’s reported Navier–Stokes proof highlights AI’s formal verification push
A blog post says OpenAI paired its reported human-readable result with a machine-verifiable Lean 4 proof, completed in 17 hours.
OpenAI has reportedly released a human-readable proof concerning the possibility that solutions to the Navier–Stokes equations can blow up in finite time, alongside a formal proof written in Lean 4.
The account, published by John D. Cook, says the Lean 4 proof was verified in 17 hours. The supplied material does not independently establish either the reported verification time or whether the underlying mathematical result resolves the long-standing Navier–Stokes problem.
The significance of the release lies in the formalisation process. Lean 4 is a proof-assistant system used to produce machine-verifiable mathematical proofs, a task that has historically required substantial manual effort.
A 2005 estimate cited by Cook suggested that formalising one page of an undergraduate mathematics textbook could take about 40 hours. Applying assumptions that research papers require 20 times more effort than textbook pages, the blog estimates that formalising OpenAI’s reported 166-page paper could have required 132,800 person-hours under older methods.
The comparison is an estimate rather than a measured general improvement, and it is unclear what portion of the broader proof-development process was included in the 17-hour figure. The post argues that lower-cost formal verification could also be applied to security policies, smart-contract liability limits and mission-critical algorithms.
