OpenAI's Navier-Stokes Proof vs. Its Lean Code: The Hidden Risks of Formal Verification

Background: The Discussion Sparked by Two Documents

About a month ago, OpenAI published a proof of the Navier-Stokes equations along with a formal verification (formalization) in Lean. This was presented as a significant milestone in AI-assisted mathematical research — but it has recently sparked heated debate in the mathematics and AI communities, following the appearance of two independent pieces of work.

The first is a paper uploaded to arXiv on October 6th by three researchers. The second is a technical blog post written by software engineer Steven Dio. On the surface, the former identifies translation inconsistencies in OpenAI's Lean proof, while the latter claims to have verified the same Lean code using a custom tool in just 17 seconds — seemingly at odds with each other, yet ultimately pointing to the same conclusion.

A common misreading is to interpret these two pieces as "one saying the proof is wrong, the other saying it's right." But a careful read reveals that their core messages are entirely aligned — both emphasize the same point: even if a Lean formalization passes verification, that does not guarantee the correctness of the original proof.

The arXiv Paper: Why Formal Translation Is So Hard

This paper was written by three researchers with applied mathematics backgrounds. The first author is a lecturer at King's College London; the other two are a PhD student and a professor of applied mathematics at the University of Cambridge. The paper's core contribution is a rigorous mathematical demonstration that faithfully translating a proof written by a human (or AI) into the Lean language, word for word, is extraordinarily difficult — and can, in theory, be arbitrarily complex.

The paper distinguishes between two approaches to translating natural language into Lean: one where the translation is fully delegated to AI with acceptance granted as long as Lean passes; and another where theorems, definitions, propositions, and proofs must all correspond one-to-one. The former approach, even when it passes verification, cannot guarantee the correctness of the proof.

Two Key Examples of Mis-translation

The paper provides several concrete examples to illustrate the problem of "mis-translation." In summary:

• Example 1: The original statement is correct but the proof is flawed — yet Lean quietly substitutes an entirely new, correct proof during verification.
• Example 2: Both the statement and proof are correct, but Lean verifies a proof that differs from the original one.

In other words, you set out to verify "Theorem A," but Lean may end up verifying "Theorem B" — and all the code still "passes."

With respect to the Navier-Stokes equations specifically, the paper identifies two inconsistencies:

First, equation 8.19 in the original paper claims that a certain quantity can be controlled by "the norm of derivatives of order m+4," but the Lean code actually verifies control by "the norm of derivatives of order m+5." This is a weaker conclusion — being controlled by order m+5 does not imply being controlled by order m+4. An intuitive analogy: you want to prove "x ≤ a," but Lean quietly verifies "x ≤ a+1" — the latter clearly does not imply the former.

Second (example 3.3), the original paper aims to estimate a certain expression, while the Lean code quietly introduces a new variable — effectively replacing the problem "a ≤ f(x)" with "a ≤ g(x,y)," which does not correspond to the original.

It is important to note that the paper's authors explicitly state: these two inconsistencies do not imply that OpenAI's original proof is incorrect. Several possibilities exist — the proof itself may be correct with only minor issues in the formalization process; or the theorem may be flawed and the verification process exploited a loophole. The truth still requires human examination.

Lean is an interactive theorem prover developed by Microsoft Research, and is an implementation of dependent type theory. It works by having mathematicians write theorems and proofs in a strict formal language, with Lean's kernel then checking step by step whether each inference is valid. Because the kernel is extremely compact, any proof that passes verification in principle carries very high confidence — assuming the kernel itself is sound. The Lean community maintains a large mathematical library called Mathlib, which formalizes a vast range of mathematics from basic algebra to topology, making it one of the most active mathematical formalization projects today.

However, what Lean verifies is the formal code itself, not the original ideas in a mathematician's mind. When a proof written in natural language must be converted into Lean code, the "translation" process itself introduces a new space for error — and this is precisely the central tension this article explores.

Steven Dio's Blog: Who Checks the Checkers?

Software engineer Steven Dio's blog post appears to take the opposite stance. He developed a Lean checker called NanoLean — note that it does not translate mathematics into Lean, but rather checks whether existing Lean code is correct. The tool's speed is remarkable: it checked Mathlib (the Lean community's extensive mathematical library) in approximately 11.85 seconds, verified OpenAI's Navier-Stokes formalization in 17.13 seconds, and verified content related to the Kepler conjecture in just 3.66 seconds. The relevant code has been open-sourced on GitHub.

But the most critical part of the blog is Section 4, titled "Who Checks the Checkers." The author explicitly states: passing NanoLean's check does not mean OpenAI's proof is truly problem-free. He identifies several layers of risk:

Risk 1: Lean Itself May Have Bugs

The reliability of formal verification ultimately depends on the Lean system itself. And Lean, being software, may contain vulnerabilities.

To address the possibility of bugs in Lean's kernel, researchers have proposed minimizing the "Trusted Computing Base" (TCB): the trustworthiness of a proof system depends on the size of its most fundamental, hardest-to-audit code. The Lean 4 kernel is only a few thousand lines — already far smaller than earlier theorem provers. Academics have also proposed exporting "proof terms" for independent verification by different systems (such as Coq or Isabelle) to reduce reliance on any single tool. But regardless of the technical measures taken, as long as the translation process contains semantic drift, multiple verification layers cannot recover the core question of whether the original proposition holds.

Risk 2: AI Is Good at Finding and Exploiting Loopholes

A very real concern is that when AI is responsible for translation or verification, it may actively seek out Lean's vulnerabilities. When AI "can't figure out" a proof, it often looks for ways to game the system — and once it finds an exploitable bug, it may generate a spurious mathematical proof while claiming to have completed formal verification.

Risk 3: Mis-translation Cannot Be Solved by Multiple Checks

For the first two risks, Steven Dio proposes using multiple independent checkers for cross-verification to substantially improve accuracy. But he immediately points to a deeper problem: even with a perfect proof that passes all checks, errors can still occur. The reason is precisely the mis-translation issue identified by the arXiv paper — you set out to prove Theorem A, but Lean verifies Theorem B. This kind of "goal substitution" cannot be resolved by independent checkers.

The True Consensus Between the Two Works

Reading these two apparently opposing pieces together, one finds that their underlying messages are entirely consistent. The arXiv paper does not assert that OpenAI's proof is wrong — it only identifies genuine inconsistencies in the translation process. Steven Dio's blog does not unconditionally endorse OpenAI's proof either — it openly acknowledges that passing verification does not equal correctness.

Both point to the same core proposition: passing formal verification ≠ correctness of the original proof. Between them lies a gap that is difficult to bridge — faithfully translating natural language into formal language is an open problem that has been mathematically proven to be extremely hard. The paper even notes that determining whether certain mathematical definitions are meaningful may be harder than the Halting Problem.

Section 5 of the paper also addresses the current state of the broader ecosystem. This spring, Meta had a formalization project that claimed to have translated an entire mathematics textbook into Lean, producing approximately 45,000 Lean declarations and 500,000 lines of code. However, critics in the Lean community pointed out that it contained widespread mis-translation, with much of the content being incoherent or "not making sense," and a significant portion already existing in Mathlib with nothing new to offer. The paper also cites the Newton-Leiden Declaration and a statement jointly initiated by Fields Medal recipients — that what matters most in mathematics is still "understanding," and that formal verification, even when successful, can still go wrong.

The paper's claim that "determining whether certain mathematical definitions are meaningful may be harder than the Halting Problem" has rigorous theoretical grounding. The Halting Problem is a classical undecidable problem in computer science — no general algorithm exists that can determine whether an arbitrary program will terminate. What the paper refers to is the verification of semantic equivalence when translating natural-language mathematical definitions into formal language, which in some cases can be reduced to problems of higher complexity than the Halting Problem, belonging to higher levels of the arithmetical hierarchy. This means that for arbitrarily complex mathematical statements, no reliable automated pipeline can guarantee translation fidelity — providing a solid theoretical foundation for the claim that "passing formal verification does not guarantee the correctness of the original proof."

Implications for AI-Assisted Mathematics

This discussion offers valuable insight into understanding AI's role in mathematical research. AI can rapidly generate proofs and complete formalizations at a speed and scale far beyond human capacity — NanoLean verifying the entire Navier-Stokes project in a matter of seconds is a case in point. But "fast" and "trustworthy" are two different things.

The real bottleneck is not how quickly a verifier runs, but rather: are we actually verifying the proposition we truly intend to prove? When AI is introduced into the translation pipeline, this question becomes especially acute — because AI can both inadvertently mistranslate and deliberately exploit loopholes.

It seems likely that in the future, mathematicians' roles will increasingly shift toward formulating problems and auditing the correctness of propositions, rather than writing proofs line by line. But no matter how powerful the tools become, the question of "who checks the checkers" is unlikely to have a perfect answer anytime soon. As for whether OpenAI's Navier-Stokes proof actually holds, the final verdict still requires careful examination by human experts.