HackerPapers

arXiv:2610.08144math.AP

Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs

Alexander Bastounis, Fabian Circelli, Anders C. Hansen

Abstract

Autoformalisation is increasingly used to verify mathematical texts, including those generated by AI, as in OpenAI's announced proof of blow-up of solutions to the Navier-Stokes equations. In this process, an AI system translates the text from a natural language (NL) into a formal language such as Lean. Once this translation is done, the argument expressed in the formal language can easily be mechanically verified. The purpose of this article is to demonstrate why this process may offer no confidence in the original NL argument, owing to the various difficulties in performing the translation semantically faithfully. In particular, we highlight that the problem of resolving ambiguities in mathematical NL text, which is necessary in order to provide semantically faithful translation, is arbitrarily high up in the Solvability Complexity Index (SCI) hierarchy/arithmetical hierarchy (the SCI $= \infty$). Hence, informally, providing semantically faithful AI autoformalisation is harder than any computational problem including the Halting problem (which has SCI $= 1$). To demonstrate the effect of this result we provide several examples of AI mistranslations of NL statements and proofs into Lean in practice, resulting in mismatches between NL proofs and their Lean `verifications'. These include OpenAI's announced Navier-Stokes proof. In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations.

arXiv comments
25 pages, 4 Figures
Journal reference
DOI
Subjects
math.APAnalysis of PDEs cs.AIArtificial Intelligence math.LOLogic

On Hacker News

Linked by 11 identifiable commenters in 11 comments across 9 threads, from Oct 2026 to Nov 2026. Found in 1 HN submission from Oct 2026 to Oct 2026. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments9 threads

  1. Egoless Mathematics in the AI Era 1 comment

    • Many of the proofs released by Open AI don’t have Lean proofs. Their system doesn’t work in Lean directly, it writes proofs in natural language first. Later, some of the proofs were passed through an auto-formalization model to generate Lean code which then passed Lean’s checks.…

      tarsierscripterView on HNParent context

  2. I know why the mathematicians weep 1 comment

    • I’ve been a math professor for about ten years, and I think people outside the field misread what makes mathematicians angry, sad, and worried. Interviews that make it into the media tend to go with “AI is killing mathematics,” maybe because that gets clicks. The reality is more…

      paulcetonView on HNParent context

  3. What mathematicians should know about the Lean Theorem Prover: reliability & AI 1 comment

    • The paper is "Navier–Stokes lost in translation" by Bastounis, Circelli, and Hansen (Cambridge/DAMTP): https://arxiv.org/abs/2610.08144

      tomkeenView on HNParent context

  4. OpenAI mistranslated mathematics into code for its Navier-Stokes proof 1 comment

    • This headline is completely wrong. The proper coding analogy is more like, the natural-language paper was the "design document" before coding it up, then when coding it up as Lean4 proofs, specific details were realized to be slightly off[1] and corrected while writing the…

      jeyView on HNParent context

  5. 'Breathtaking,' 'Devastating': Mathematics Reels After New OpenAI Release 1 comment

    • I read somewhere that 56% of the problems had some Lean Proof, but upon inspection, there are gaps between what Lean proves and what English says about the proof. Making an English language description of a problem and proof steps match the Lean proof is apparently harder than…

      gregw2View on HNParent context

  6. Ask HN: What if no AIpocalypse, no AI bubble, what if it just keeps advancing? 1 comment

    • Until models have taste, we still need Software Engineers to judge their output in the context of a broader goal. Not saying this will never happen, but we have yet to see evidence of models getting good at this. If anything, the lack of improvement on that axis has been quite…

      pierreb-aivaView on HNParent context

  7. OpenAI withdraws three mathematical results 2 comments

    • Oh I fully understand how Lean works, how minimal the kernel is etc. I just think that just because "it compiled", we don't actually know that the autoformalization proved all the right stuff along the way. After all, LLMs can produce correct proofs for statements that don't…

      ijustlovemathView on HNParent context

    • > All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code. That's exactly what the navier stokes paper posted yesterday pointed out where the LLM bends the…

      persedesView on HNParent context

  8. “Math 2.0” will need to value mathematical progress more holistically 1 comment

    • There is no guarantee that the lean proof is 1:1 with the natural language equivalent. The lean proof can be lesser. This happened in the Navier-Stokes proof, e.g. see [1] in example 3.1. Having the certificate doesn't necessarily imply correctness. [1]…

      cmceangaView on HNParent context

  9. The Mathocalypse 2 comments

    • There's an entire paper claiming that many of these AI-generated Lean proofs are formulated incorrectly / mistranslated: https://arxiv.org/abs/2610.08144

      nperez19View on HNParent context

    • In addition to those issues that the wife in the story raised, here's some meta-analysis of the Navier-Stokes result that puts all of these solutions into question: https://arxiv.org/abs/2610.08144 > Autoformalisation is increasingly used to verify mathematical texts, including…

      dualvariableView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.