OpenAI just solved Navier-Stokes. Or did they?
OpenAI's Lean formalisation of their AI proof shows that the code compiles, but it does not show that their natural language argument is correct. AI proofs are useful as guides, yet people must still read and verify them, especially when the text is long (and convoluted).
Read article >