On September 10, 2026, OpenAI announced a proof that addresses a long-standing question regarding the Navier-Stokes equations in fluid dynamics. Alongside the conventional proof, OpenAI also released a Lean 4 formal proof, which has not been widely discussed. Recent advancements in AI have led to the resolution of several mathematical conjectures, often accompanied by formal proofs using Lean 4.
Historically, generating machine-verifiable formal proofs has been a labor-intensive process. According to Henk Barendregt and Freek Wiedijk, formalizing one page from an undergraduate mathematics textbook could take approximately one work-week, or 40 hours. Given that research publications are denser than textbooks, it is estimated that formalizing a research article could take up to 20 times more effort. For instance, formalizing OpenAI's 166-page paper would theoretically require about 132,800 person-hours. However, OpenAI managed to verify their proof in Lean in just 17 hours, marking a significant reduction in the time and effort required for formal verification.
The implications of formal verification extend beyond mathematics. It can be applied to ensure the consistency of security policies, verify the maximum liability of smart contracts, and confirm the correctness of critical algorithms, which are generally easier to formalize than mathematical research and offer a clearer return on investment.