GoKawiilCambridge mathematicians flag mismatch in OpenAI's Navier-Stokes proof versions
OpenAI's September 8 announcement of a solution to the Navier-Stokes problem included two versions of its proof: one in natural language with mathematical symbols, and one formalised in the Lean programming language for automated verification. A team led by Anders Hansen and Fabian Circelli at the University of Cambridge says these two versions do not actually match, meaning the Lean code may not faithfully represent the natural-language argument.