Navier Stonks Lost in Translation | Informal Proof ≠ Lean Proof (but statement still correct!)

Summary
In this video, researcher Alex Hyman reviews the paper “Navier-Stokes Lost in Translation: Why Lean Verification of AI Autoformalisation Does Not Guarantee Correct Natural Language Proofs” by A. Bastounis, F. Circelli, and A. C. Hansen. He examines the distinction between autoformalising an informal mathematical claim to produce a verified Lean theorem versus generating a semantically faithful formal translation of the informal paper’s actual proof steps. Through whiteboard demonstrations and analysis of OpenAI’s Navier-Stokes blow-up claim and Meta’s textbook formalisation efforts, he explores why machine-checked Lean code does not automatically validate natural language proofs and outlines the fundamental computational limits of autoformalisation.

What is shown

• [00:11] Display of the title and author block of the paper “Navier-Stokes Lost in Translation” by A. Bastounis, F. Circelli, and A. C. Hansen.
• [00:58] Lean 4 code showing the declaration of theorem navier_stokes_breakdown_R3.
• [03:34] Terminal capture showing Lean checking over 9,000 files/declarations (9,017/9,371 built) in the Navier-Stokes repository.
• [04:40] Text excerpt from the paper defining task (i): translating an alleged natural language proof into Lean without sorry or extra axioms.
• [05:03] Example text of Cantor’s theorem rendered in the Naproche natural proof assistant.
• [07:26] Whiteboard layout contrasting informal statements and proofs against formal Lean statements and proofs.
• [14:12] Warning excerpt from the paper stating that a compiling translation does not guarantee the original natural language proof is correct.
• [16:01] Whiteboard demonstration using the cubic polynomial $P(x) = x^3 - x^2 - x + 1 \ge 0$ for $x \ge -1$, contrasting an invalid factorization argument $(x+1)^2(x-1)$ with the valid one $(x+1)(x-1)^2$.
• [18:28] Prompt submitted to ChatGPT asking to formalise the incorrect factorization argument into Lean, showing how the LLM silently repaired the algebraic identity to produce compiling Lean code [18:37].
• [23:20] Paper excerpt of Example 2.2 analyzing real symmetric matrix trace inequalities ($\text{tr}(A^2) \ge 0$), highlighting how the AI generated a direct entry-wise proof rather than the author’s orthonormal eigenbasis proof.
• [26:30] Excerpts of Example 3.1 and Example 3.3 from the paper showing discrepancies between OpenAI’s paper estimates (e.g., derivative loss in inverse estimates and pressure-flux bounds) and the actual Lean formalisation.
• [30:03] Excerpt of Remark 3.4 displaying experimental findings using Claude and ChatGPT to flag potential mistranslations in OpenAI’s proofs.
• [36:33] Pseudocode while-loop illustrating an iterative autoformaliser repairing candidate Lean proofs until they compile.
• [44:34] Whiteboard derivation of polynomial enumeration and the construction of $r_e = 1 / (n_e + 1)$ connected to undecidability via Hilbert’s 10th problem.
• [50:02] Excerpts from Section 5 discussing Meta’s Spring 2026 attempt to formalise 26 math textbooks, the June 2026 Leiden Declaration on AI in mathematics [51:17], and the September 2026 declaration “A Severe Misalignment of AI in Mathematics” signed by Fields Medalists [51:33].

Claims & numbers

• The presenter notes that OpenAI’s Lean codebase for the Navier-Stokes project contains over 9,000 individual components to build and verify [03:34].
• The presenter explains that while the top-level Lean theorem statement navier_stokes_breakdown_R3 faithfully captures the existence of a finite-time blow-up, intermediate lemmas (such as Lemma 8.6 and equation 10.19) in OpenAI’s written paper feature different or stronger bounds than what was verified in Lean [26:30, 27:30].
• The presenter cites the paper’s reduction to Hilbert’s 10th problem (for polynomials in $k \ge 9$ variables) to argue that an AI autoformaliser cannot generally decide when mathematical terms are well-defined, making faithful semantic autoformalisation strictly harder than the halting problem [48:06, 51:31].
• The presenter references Meta’s Spring 2026 claim of formalising 26 mathematics textbooks into ~45,000 declarations and ~500,000 lines of Lean code, noting community pushback that reported zero tested target statements were accurately formalised without fatal errors [54:40, 55:02].
• The presenter quotes the September 2026 declaration by 25 Fields Medalists warning against overemphasizing automated “true/false” problem solving at the expense of conceptual insight [56:33].

Notable quotes

• [01:26] “Navier-Stokes does blow up, but the argument that you would read on pen and paper may or may not be trusted.”
• [14:12] “Meeting the success criterion of (i) does not mean that the original NL proof is correct.”
• [48:06] “No, such an AI autoformaliser can never exist, even if one could solve the Halting problem.”

Assessment
This video is a detailed analytical review and educational commentary by a researcher in formal verification. The presenter provides an authentic whiteboard lecture paired with on-screen paper excerpts, verifiable Lean code, and direct LLM outputs without misleading staging or exaggeration.

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