Navier–Stokes Lost in Translation
- ID
- 33163
- Status
- summarized
- Published
- 07 Oct 2026, 11:24 PM
- Fetched
- 08 Oct 2026, 8:01 PM
- Provider
- Hacker News
- Category
- dev-community
- Original URL
- https://arxiv.org/abs/2610.08144
- Source URL
- https://hnrss.org/best
Summary
- Score
- 6.5
- Created
- 08 Oct 2026, 8:01 PM
- Tags
- Audience
- developersai_ml_learnersai_agent_users
What happened
A 25-page arXiv paper (2610.08144, submitted 6 Oct 2026) by Alexander Bastounis, Fabian Circelli and Anders C. Hansen argues that AI autoformalisation — translating natural-language maths into Lean so it can be mechanically checked — cannot give confidence in the original natural-language argument. The authors claim that resolving ambiguity in mathematical prose is arbitrarily high in the Solvability Complexity Index hierarchy (SCI = ∞), making it harder than any computational problem including the Halting problem (SCI = 1). They give examples of AI mistranslations into Lean in practice, including stating that the formalised Lean proof of OpenAI's announced Navier–Stokes blow-up result does not correspond to the natural-language proof of blow-up.
Why it matters
If you treat Lean (or any formal checker) as a trust layer for AI-generated artefacts, this paper says the checker only certifies the formal statement it was handed, not that the formal statement means what the original text said — and the translation step is the one shown to be unverifiable in general. Concretely, a green Lean check on an OpenAI-style claim tells you nothing until a human reads the natural-language-to-formal mapping, so any pipeline where an agent writes a spec and a tool 'verifies' it needs a human step on the translation, not on the proof. The paper names OpenAI's Navier–Stokes announcement as a case where that mapping broke.
Discussion angle
The paper puts ambiguity resolution at SCI = ∞, above the Halting problem — so is 'verified AI output' ever a real claim, or should every formal-verification demo for AI-generated code be judged on the spec-translation step instead? Ask the room where their own agent pipelines assume a checker proves intent.