OpenAI mistranslated mathematics into code for its Navier-Stokes proof
Summary
New Scientist reports that OpenAI published two proofs of the Navier-Stokes problem a natural language version and a Lean formalization intended for machine verification. The Lean code does not match the natural-language proof, a discrepancy highlighted by researchers from Cambridge. The case, including a specific mismatch around Lemma 8.6 and a weaker bound, shows that AI auto-formalisation can diverge from human reasoning and cannot yet replace peer review. OpenAI says it will rectify errors in the natural-language version and continue formalising more papers.