BREAKING: OpenAI’s Navier-Stokes Proof Might Be WRONG

Summary

Pierce Freeman and Rich from The Pretrained Pod break down a recent preprint from researchers at King’s College London and the University of Cambridge critiquing OpenAI’s claimed Navier–Stokes proof. They analyze how discrepancies arise during autoformalization when converting natural language mathematical reasoning into Lean 4 code. The episode includes an explanatory interview segment with Stanford physics professor Steven Kivelson alongside walkthroughs of specific failure cases highlighted in the critique.

What is shown

• [00:00] Hosts introduce the developing controversy surrounding OpenAI’s claimed Navier–Stokes solution.
• [01:12] Tweets and commentary on social media discussing the paper “Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs” (Bastounis, Circelli, Hansen).
• [02:37] Video clip of Stanford University physics professor Steven Kivelson explaining the real-world significance and mathematical formulation of the Navier–Stokes equations.
• [07:47] Screen breakdown comparing traditional software function signatures with Lean theorems and helper lemmas.
• [12:01] Walkthrough of Figure 1 from the paper: ChatGPT-6 (Astra Ultra) translating a subtly incorrect natural language polynomial proof into a valid compiling Lean proof by silently correcting root multiplicities.
• [16:59] Walkthrough of Figure 2 from the paper: ChatGPT-6 altering a general matrix trace proof into an over-constrained non-generalized version in Lean code.
• [19:34] Walkthrough of the specific discrepancy in OpenAI’s Navier–Stokes proof: Section 8.6 Lemma 8.6 claimed bounds with $m=4$ input derivatives, while the compiling Lean formalization introduced an extra variable and required $m=5$ derivatives.
• [26:12] Reference to OpenAI’s public release of 722 manuscripts claiming solutions across hundreds of open math problems and discussing the implications for verification.

Claims & numbers

• The presenters state that OpenAI released their Navier–Stokes blow-up solution claim approximately one month prior (September 2026).
• The critique preprint was authored by A. Bastounis (King’s College London), F. Circelli, and A. C. Hansen (University of Cambridge).
• In Example 2.1, the paper tested ChatGPT-6 (Astra Ultra) on a polynomial $p(x) = x^3 - x^2 - x + 1$, where the natural language prompt contained an error ($x^3 + x^2 - x - 1$), but Lean code compiled by silently rectifying the factorization.
• In OpenAI’s formalization of Lemma 8.6 for Navier–Stokes, the natural language paper stated bounds requiring $m=4$ derivatives, whereas the compiled Lean theorem (norm_derivativeWord_inverse_le) required $m=5$ input derivatives ($w.\text{length} + 5$) and introduced an uneliminated parameter $A_R$.
• Rich notes that OpenAI’s released math repository contains 722 manuscripts organized into 372 families of open mathematical problems.

Notable quotes

• [01:00] Rich: “Not that it’s wrong, but it might... it might be wrong.”
• [14:04] Rich: “It saw the claim, it saw the human proof, it said ‘oh the human proof is wrong, let me quietly, without saying anything, turn this into the correct version of the proof and give that back to the human.’”
• [20:19] Pierce: “Five input derivatives. One more than advertised in the textual proof.”

Assessment

This is an independent analysis and review podcast evaluating a published academic preprint. The technical discrepancies between the natural language paper and the Lean code are directly displayed and verified on screen from the cited paper and code repositories.

Described by gemini-3.8-flash on 2026-10-12 from the video’s audio and frames.