OpenAI's Lean 4 proof cuts formal verification from 132,800 hours to 17
The part of Navier-Stokes no one is talking about
OpenAI's proof of a long-standing Navier-Stokes question came with a Lean 4 formal proof, a detail few have discussed. Formalizing one page of an undergraduate math textbook once took about 40 hours; scaling that to OpenAI's 166-page paper would mean 132,800 person-hours. OpenAI verified its proof in Lean in just 17 hours—a four-orders-of-magnitude drop. The same approach could verify security policies, smart contracts, and mission-critical algorithms, where ROI is easier to quantify.
I hesitate to use the word “revolutionary,” but lowering the cost of anything by four orders of magnitude is revolutionary.
- stabbles
It's kinda funny to realize that Lean is apparently so slow that for Fermat's Last Theorem proof verification runs only 1 order of magnitude faster than agents could generate the Lean code (15h verification with 230GB of RAM vs 11 days to generate it).
To what extent can you optimize Lean? It has to be simple enough to be auditable, does that mean you cannot use opaque optimizations to make it run faster?
- parhamn
They estimated $40M of agent costs (it was a large fleet of them). Using the number in the post its closer to ~880,000 hours × $150/hour = $132 million for the human case. Still an amazing feat not quite "four orders of magnitude". The comparison is obviously pointless because coordinating 1M hours of intellectual labor isn't easy to say the least.
Very exciting and uncertain times!
- boshalfoshal
People seem to be talking about anything except the actual results with this particular announcement.
Its still astonishing that any sort of generalized computer program can solve a problem of this magnitude, and we have witnessed it happening in real time. I'd be curious to see if the new model can also do more direct proofs/inductive proofs.
- pkal
IMO the "forty hours per page" rule is not up to date, and more a consequence of lacking proof automation in 2005. From what I understand about Lean, this has been one of the things that they have put a lot of effort into improving, making proof mechanization more palatable to the mathematically inclined, as opposed to just logicians.
- lordnacho
How do you know that it's formalizing what you think it's formalizing? If your Lean 4 has a bug, won't you be proving something other than what you thought?
- 3m4r
Not necessarily applied to OpenAI's solution to Navier-Stokes, but what happens if and when an AI genuinely appears to solve an extremely difficult problem but humans cannot independently verify the solution because understanding the proof/argument requires intelligence the verifiers biologically don't have or the resources to afford to use automated tools?
We've already seen evidence in the wild of agents attempting to bypass doing the actual work in bench-marking (aka just steal the answer key) due to the perceived economy in cheating to get results. What happens if or when we no longer have the capacity to actually detect either AI cheating or simply a wrong answer? What happens if there's a long-play social engineering attack (like the attempted XZ takeover) of something upstream of a core tool (or its dependencies) for formal verification and we have no trusted computing base?
Which would be cheaper and a more direct path, especially in the long run? Those trying to build a rock-solid castle need to defend thousands of potential gaps; the attacker needs to find only one.
- zem
not to take away from the author's appreciation of newly accessible formal proofs, but people have been talking about the savings in formalization effort for longer than they have been talking about the AI doing the actual proofs!
- aabhay
Formalizing proofs in Lean has gotten dramatically easier since the formalizations available in 2005. And Lean’s mathlib has done most of the underlying work so that you have its axioms and necessary lemmas baked in. You can think in terms of standard abstractions that look very much like the exact notation in the undergrad textbook.
That said, I am not in any way trying to discount how incredible of an achievement it is to formalize a millennium prize winning algorithm in Lean. I mean just look at the code that OpenAI published. It’s like an encyclopedia of different fluid dynamics concepts.