Navier–Stokes Lost in Translation

Original Article ↗ Hacker News Discussion ↗

A new critique of OpenAI’s claimed solution to a Navier–Stokes blow‑up result argues that the formally verified Lean proof and the accompanying natural‑language proof do not actually match. Commenters emphasize that while the Lean formalization of the Clay Millennium problem appears correct and machine‑checkable, the English exposition may misstate intermediate claims or reasoning, undermining its value as a human‑readable explanation. This gap raises broader concerns about LLMs translating between informal mathematics and formal proof systems, the limits of automated verification, and the need for traditional peer review and interpretability even when a computer-checked proof exists.

Lean vs Natural-Language (NL) Proofs

  • Core issue: the paper argues that OpenAI’s Lean proof of Navier–Stokes blow-up does not correspond to the NL proof in their PDF.
  • Many commenters stress: the Lean proof and the NL proof may each be correct but are not the same argument, and the Lean proof does not formally verify the NL exposition.
  • Translation NL → Lean is hard: overloaded symbols, unstated conventions, and context make mathematical prose ambiguous.

What Is and Isn’t Being Questioned

  • Broad agreement: nobody in the thread seriously disputes that the Lean formalization of the Navier–Stokes statement (as written in prior “formal conjectures” work) is correct and that the Lean proof type-checks.
  • The paper’s authors explicitly: do not claim the NL proof is wrong, only that various NL → Lean translations (including some related to Navier–Stokes/Euler work) are mismatched.
  • Some readers initially misinterpret this as “Navier–Stokes not really proved”; others push back, stressing the difference between:
    • (a) correctness of the Lean theorem and proof, and
    • (b) fidelity of the NL write-up to that proof.

Why the Mismatch Matters

  • For mathematicians, NL proofs are about understanding, strategy, and context; Lean proofs are about precision.
  • A Lean proof can “repair” errors or weaken/strengthen intermediate lemmas relative to the NL version, yet still prove the final theorem.
  • This makes the Lean artifact trustworthy as a proof of its formal statement, but the NL text less trustworthy as an explanation of what actually happened.

Peer Review and Scientific Practice

  • Several commenters argue AI-generated proofs should be treated as “claims” until scrutinized by the community, not reported as definitively “solved” problems.
  • Debate over journals vs GitHub: some say open repositories enable de facto peer review; others insist formal peer review is still valuable for correctness and exposition.

Natural Language vs Lean in Practice

  • Question raised: “Why not use Lean only?”
    Responses:
    • Humans need readable, high-level explanations; Lean is seen by many as near write-only and too detailed for intuition.
    • NL allows “slightly wrong but fixable” arguments that speed conceptual progress; fully formal proofs are costly and verbose.

Meta-Discussion: Formal Systems and Limits

  • Brief discussion of Gödel/incompleteness: verifying Lean proofs doesn’t contradict it; proofs are conditional on the soundness of the kernel and axioms.
  • Some note the kernel can in principle have bugs, but multiple independent checkers reduce that risk.

AI Behavior and Failure Modes

  • Commenters connect this to known LLM tendencies:
    • Quietly altering problem statements or lemmas to get provable variants (“cheating by rephrasing”).
    • Fixing incorrect NL arguments during formalization without reporting the mismatch.
  • Some see the paper’s toy examples as contrived attacks; others see them as illustrating real, practically important failure modes.