Yesterday OpenAI announced a proof that settled a long-standing question about the Navier-Stokes equations from fluid dynamics. The announcement has created a lot of buzz, as one would expect. But there’s an aspect of OpenAI’s work that I haven’t seen anyone talk about: they posted a Lean 4 formal proof at the same time as their conventional human-readable proof.
Quite a few other mathematical conjectures have been settled recently using AI, and these have also been accompanied with formal proofs, using Lean 4 in particular.
Until very recently, generating machine-verifiable formal proofs has been excruciatingly tedious. In 2005, Henk Barendregt and Freek Wiedijk wrote
To give an indication of how much work is needed for formalisation, we estimate that it takes approximately one work-week (five work-days of eight work-hours) to formalise one page from an undergraduate mathematics textbook.
That was the rule of thumb: forty hours per page. And this in the context of undergraduate textbooks. Research publications are much denser than textbooks. Furthermore, page 100 of a textbook probably depends mostly on material on pages 1 through 99. A sentence in a research article could cite anything that has been published before.
Say a research article takes 20 times more effort to formalize than page in an undergraduate textbook. Then formalizing the 166-page paper from OpenAI would take 132,800 person-hours. It took OpenAI 17 hours to verify their proof in Lean. I hesitate to use the word “revolutionary,” but lowering the cost of anything by four orders of magnitude is revolutionary.
I’ve used AI to generate formal proofs to check my work just for a little blog post. I wouldn’t dream of doing that if I had to pay someone a week’s salary to check my work.
Formal verification doesn’t just apply to mathematics. You could, for example, formally verify that a set of security policies are consistent and that, given certain assumptions, they accomplish their purpose. You could formally verify that a smart contract imposes a certain maximum liability. You could verify the correctness of mission-critical algorithms. These problems are easier than formalizing mathematics research, and it is easier to quantify the return on investment.
The work you describe on security and policy is an enormous, juicy, sweet spot.
Work on, roughly, “formalized bug finding” has been done by Google and AWS (e.g. S3 and DynamoDB performance verification, TPU design) and goes back well over a decade. TLA+ was used a lot, and from what little I know, using TLA+ makes using LEAN look like a walk in the park.
It works, and its been in play for years. But (again roughly) ‘adversarial bug finding’ is not full verification that you speak of. On the backend, as far as i can tell, every single one of the formal verification tools is some flavor of SAT/SMT solver. Glad it’s “mainstream” now. Good times.
Dan Bernstein (“Papers with computer-checked proofs”, written 2023 originally) discusses his experience with proof assistants and/or checkers, and gives some other quotes about the expected time to formalize (your data from 2005 is a bit old, but it’s still close to ballpark).
I think this a strange perspective. The formalized proof was developed iteratively in Lean using Prove2Me (https://prove2.me/), a kind of gamified version of previous proof blueprint tools, to coordinate and maintain a DAG of proved and open subgoals. Anthropic’s announcement states “The effort succeeded when we switched to using Prove2Me”. Now, prior to that they were targeting a Lean proof but the LLM agents couldn’t keep track of what they’d proved. Without a Lean proof how could they certify the result, or be confident of it in any way?
The real point here is that, as steve@discuss.systems (on Mastodon) wrote:
“The entirety of the achievement is the infrastructure that allows us to validate LLM output constrained to (subfields of) mathematics.”
The cost collapse is the interesting part, but I think the practical bottleneck moves rather than disappears.
Formal verification answers “did I implement what I wrote down?” It doesn’t answer “did I write down the right thing?” That specification gap is exactly where the expensive human work sits for the use cases you list — security policy consistency, smart-contract liability caps, mission-critical algorithms. Cheaper proofs make it much easier to iterate on the statement, though, which makes that gap smaller in practice than it used to be.
The other thing that changes: review becomes diffable. Two proof states, a checked artifact you can point at, instead of an argument in prose that has to be re-derived every time someone new reads it.
The Open AI Lean formalization process for NV used around $1 or $2 million dollars of compute. That dollar value is roughly 10,000 human mathematician hours. Your estimate of “132,800 person-hours” to formalize the NV proof would cost around ten times as much as paying the Open AI LLM to formalize it.