OpenAI's Lean Verification Doesn't Actually Prove Its Navier-Stokes Breakthrough
A new arXiv paper argues that passing a Lean check gives no guarantee the original natural language proof is right, and uses OpenAI's Navier-Stokes claim as exhibit A.
- New arXiv paper argues Lean verification does not imply the English proof is correct, using OpenAI's Navier-Stokes announcement as evidence.
- Authors prove semantic faithfulness of autoformalisation sits at SCI = infinity, harder than the halting problem.
- Three failure modes identified: silent fixes, divergent proofs, and formal statements weaker than NL claims.
- Concrete mismatches shown in Lemma 8.6 and pressure-flux bound (10.19) of OpenAI's manuscript.
- OpenAI's proof used roughly 10,000 agents over 88 hours, with GPT-6 Astra formalising in Lean in 17 hours.
- Takeaway: "Lean verified" labels on AI-generated math require human scrutiny of the translation step, not just the compile.
A Lean Build Does Not Verify an English Proof
OpenAI paired a 166-page manuscript with a Lean 4 project when it announced the result: an internal model had allegedly proved finite-time blow-up for the three-dimensional Navier-Stokes equations. Blow-up means that a smooth fluid solution develops a singularity in finite time. A valid construction under the required conditions could resolve the breakdown branch of a Clay Millennium Prize problem. OpenAI presented the formalisation as strong evidence for the manuscript, but Alexander Bastounis, Fabian Circelli and Anders C. Hansen argue in a new paper that compilation certifies the Lean file without certifying its correspondence to the English argument.
What the kernel actually checks
Autoformalisation converts mathematical prose into formal statements and proof terms for an interactive theorem prover. Current systems combine language models with retrieval, generated code and compiler feedback. Lean then checks whether each proof term has the declared type under the project’s definitions, assumptions and axioms. Comparing those declarations with the source manuscript remains a separate review task.
| Question | Required evidence |
|---|---|
| Does the formal theorem follow from its stated assumptions? | A successful Lean kernel check under a documented toolchain. |
| Does the formal theorem encode the manuscript’s claim? | A statement-by-statement semantic audit by mathematicians. |
| Does the formal proof represent the manuscript’s argument? | A mapping between informal steps and Lean declarations. |
| Does the project rely on placeholders or added axioms? | An audit for sorry, custom axioms and dependencies. |
This story is for Pro members
You've reached the end of the free preview. Upgrade to AlphaSignal Pro to read the full article - and everything else behind the paywall.
Comments
