OpenAI posts Lean 4 proof alongside its Navier-Stokes result
- OpenAI released a Lean 4 formal proof alongside its human-readable Navier-Stokes proof, and the post says Lean verified the proof in 17 hours.
- The author applies a 2005 estimate of 40 work-hours per undergraduate textbook page and assumes research formalization takes 20 times more work, producing an estimate of 132,800 person-hours for OpenAI's 166-page paper.
- The post says other mathematical conjectures settled recently with AI have also been accompanied by machine-checkable proofs, particularly in Lean 4.
- The author argues that lower formalization costs could make formal checks more practical for security policies, smart-contract liability limits, and mission-critical algorithms.
Hacker News opinions
People have discussed the drop in formalization effort longer than they have discussed AI generating the proofs. The accessibility angle is not new.
The agent run reportedly cost about $40M. Using the post's assumptions, the human comparison is closer to 880,000 hours at $150 per hour, or $132M, so it is impressive but not four orders of magnitude cheaper.
I do not think the 40-hours-per-page figure remains current. Lean automation and mathlib have made mechanization far less painful than it was in 2005.
I am amazed that a general-purpose program can handle a problem of this scale. I would like to know whether the model can also produce more direct or inductive proofs.
That conclusion depends on where the model got its ideas. If it trained on, or accessed, rough notes from researchers already close to the result, turning those into a complete Lean proof is still notable, but it changes the claim about discovery.
I have a math bachelor's degree and could not begin to follow either the human proof or the LLM proof without a huge time investment. Most people discuss prompt training choices because those affect them more directly than Navier-Stokes.
The compute bill matters too. I have seen estimates around $10M, enough to fund 20 to 25 researchers for five years, so this remains out of reach for most groups even if costs keep falling.
The plagiarism question is central, not a side issue. If agents assembled unpublished work by other researchers, we cannot tell how much of the result was genuine innovation until that is resolved.
Lean formalization is much easier now, and mathlib already supplies many axioms and lemmas in notation close to undergraduate texts. Still, formalizing a Millennium Prize-level result is extraordinary, and the published code spans a huge amount of fluid-dynamics material.
Lean verification itself is expensive. Fermat's Last Theorem reportedly took 15 hours and 230GB of RAM to check, versus 11 days for agents to generate the Lean code, and I wonder how far performance can improve without making the checker too opaque to audit.
That comparison may ignore hardware and parallelism. The agents likely used a large inference cluster and repeatedly ran the verifier, while the final Lean check may have run on one machine, so the actual compute gap could be much larger.