Navier–Stokes Lost in Translation
4 hours ago
- Autoformalisation is used to verify mathematical texts by translating natural language (NL) into a formal language like Lean, but this process may not guarantee the correctness of the original NL argument.
- Semantically faithful translation of mathematical NL is extremely difficult, with the problem of resolving ambiguities having a Solvability Complexity Index (SCI) of infinity, making it harder than the Halting problem.
- Examples of AI mistranslations of NL statements and proofs into Lean are provided, including OpenAI's announced Navier-Stokes proof, where the formalised Lean proof does not match the original NL proof of blow-up of solutions.