In cracking one of the biggest unresolved problems in mathematics, OpenAI launched a controversy over the information it used to train the developmental artificial intelligence system behind it, which raises questions over to whom credit for the accomplishment belongs. The controversy is overshadowing AI's more important contribution to the advancement of mathematics: its role in "autoformalizing" mathematical proofs in the Lean proof assistant.

Autoformalization refers to the automated formal verification of a mathematical proof utilizing proof assistant software. That matters because developing the computer code to verify a proof is often a time consuming and often tedious task for mathematicians.

As a general rule of thumb, it takes 40 hours of labor for a mathematician to formalize the equivalent of one page of an established mathematical proof presented in a textbook with all supporting material preceding it using the popular Lean proof assistant. John D. Cook, an applied mathematician and statistician who runs a consulting firm, estimates a research paper in mathematics takes about 20 times more effort to formalize into a Lean-verified proof, mainly because time needed to collect and validate all the supporting material for it, which may or may not be presented within the paper.

OpenAI's Navier-Stokes proof runs 166 pages. By Cook's back-of-the-envelope math, formalizing all the math needed to verify it could take as much as 132,800 hours for mathematicians to execute.

OpenAI autoformalized its Navier-Stokes proof in just 17 hours.

It's also not just OpenAI's technology making these kinds of advancements toward automating the most tedious and time consuming aspect of modern mathematics. On 4 September 2026, less than a week before OpenAI unveiled its Navier-Stokes proof, Anthropic announced its Claude AI system had successfully generated Lean-verified code for Andrew Wiles' proof of Fermat's Last Theorem (FLT). In doing so, Anthropic beat the mathematicians who had been working for years to formalize it by manually coding it in Lean.

Here's how Anthropic describes what its Claude AI system accomplished:

One way to check a proof’s correctness is to ask a computer to do it. Proof assistants like Lean verify the logic of a proof algorithmically, demonstrating its correctness beyond a doubt. The difficult part for humans is rewriting the proof so Lean can understand it. While a proof written for human readers will skip many obvious steps, Lean needs to see every step, no matter how trivial. Human proofs also build on centuries of published work, while a formalization starts from the tiny fraction of math that’s been formalized already.

For FLT, the formalization process was expected to take years. Just the blueprint the mathematical community has been using to describe the initial phase of the project runs to 86 pages.

Claude completed the proof in 11 days, producing computer-verifiable proofs of 30,300 theorems along the way (using 29,500 in the final proof). Dozens of Claude agents collaborated to define concepts, prove intermediate theorems, and use those theorems to prove ever harder statements. At 13 million lines of Lean code, Claude’s proof is over 5x the size of Mathlib, the principal community library of mathematical proofs this theorem builds on.

Here's some more back of the envelope math. If mathematicians were given $20 million and told to generate the Lean code to verify the Navier-Stokes proof using 132,800 hours of labor, no more and no less, assuming they got it done, they would effectively be paid a little over $150 for each hour of labor. That may even be close to what it would actually cost a single trained mathematician or coder per hour of their labor. Although assuming they worked 40 hours a week, 50 weeks a year, it would also take them nearly 64 years to perform the task.

How many trained mathematicians do you think it might take to accomplish the same task in 17 hours? Keep in mind that level of execution would also take extraordinary planning, preparation, coordination, and execution on their part to accomplish the task in that time. Do you think that extraordinary effort would cost more or less than $20 million?

Businesses around the world are already running numbers like these. The potential to realize massive savings in time and cost is why AI technology has sparked an investing and development boom in the last few years. It might have cost OpenAI $20 million to develop its AI systems to crack the Navier-Stokes equations including generating the Lean code to verify the proof, which perhaps appears excessive next to the Clay Mathematical Institute's $1 million prize for the achievement. But how much would the alternative of having an army of trained mathematicians to do the same job in the same time have cost?

Previously on Political Calculations

We've been covering developments toward the resolving the open question of when the Navier-Stokes equations describing fluid motion works and when it doesn't for some time. Here's our coverage in chronological order:

• The Biggest Math Story of 2017
• The Biggest Math Story of 2018
• Navier-Stokes and the Emergence of Order from Disorder
• What is Emergence?
• The Biggest Math Story of 2019
• A Proof for Batchelor's Law
• The Biggest Math Story of 2022
• Breakthrough in Unifying Math to Describe How Fluids Behave at Different Scales
• The Biggest Math Story of 2025
• AI Cracks the Navier-Stokes Millennium Problem, Part 1
• AI Cracks the Navier-Stokes Millennium Problem, Part 2