Lean 4 Formal Proof Included in OpenAI's Navier-Stokes Announcement

OpenAI released a Lean 4-based formal proof for the Navier-Stokes equations, demonstrating the efficiency of AI-assisted mathematical formalization. This is evaluated not merely as the completion of a proof, but as a case that significantly improved the economic viability of formal verification.

Dramatic Reduction in Formalization Costs

Previous research estimated that formalizing one page of a research paper required 2,656 hours, which is about 20 times the effort for a textbook page. Applying this standard to OpenAI's 166-page paper would require approximately 132,800 person-hours.

However, OpenAI utilized LLMs to complete the verification of the proof in just 17 hours. This represents a cost reduction of approximately four orders of magnitude (1/10,000 level) compared to previous estimates. While some analyses estimated the actual computing costs at approximately $1 million to $2 million, it is described as 'revolutionary' for replacing the labor equivalent to 10,000 hours of human mathematicians.

Technical Approach and Limitations

• Introduction of Prove2Me: Similar to Anthropic's case, gamified tools like Prove2Me and subgoal infrastructure played a key role in tracking and managing proofs generated by LLMs.
• Gap Between Verification and Specification: Although lower costs have made proof iteration and review easier, the specification gap—determining whether 'what was intended was accurately specified'—remains a human domain.
• Scalability: Beyond mathematical research, the scope of application is expected to expand to areas where formal methods can easily achieve ROI, such as consistency verification for smart contracts, mission-critical algorithms, and security policies.