science
Preprint challenges Lean verification of OpenAI’s Navier–Stokes proof
A mathematics preprint argues that Lean’s verification of a formal proof does not guarantee that the proof faithfully represents the original natural-language argument. The authors say this mismatch occurs in the formalisation of OpenAI’s announced Navier–Stokes blow-up proof.