Navier–Stokes Lost in Translation

	Navier–Stokes Lost in Translation(arxiv.org)
	337 points by nill0 6 days ago \| 210 comments
	tl;dr: The authors argue that AI autoformalisation—translating natural-language math into Lean for mechanical verification—provides no real confidence in the original argument, because resolving ambiguities in mathematical prose is provably harder than any computational problem (infinite on the Solvability Complexity Index, versus 1 for the Halting problem). They demonstrate this with concrete mistranslations, including OpenAI's recently announced Navier-Stokes blow-up proof, showing the Lean "verification" does not actually correspond to the natural-language proof it claims to formalise.
	HN Discussion: ↑Highlights the bombshell claim that OpenAI's Navier-Stokes proof may not be properly formalized ~Questions whether the mismatch matters if the Lean theorem still matches the original Clay Institute statement ↓Dismisses the paper as overblown since NL-to-Lean translation naturally allows multiple valid forms ↑Agrees the LLM altered the proof substantively rather than merely resolving ambiguity •Clarifies scope: authors only critique translation, not OpenAI's underlying NL proof correctness