Re: Navier–Stokes Lost in Translation

No, they're not claiming that.

No one is disputing that the Lean formaization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.

The authors are claiming that the Lean proof is not the same proof as the NL one. Therefore, we shouldn't yet have confidence that the NL proof is valid.

This is an important claim which the math community will need to work through. However, the Lean proof alone is sufficient for OpenAI to (reasonably confidently, leaving aside questions of academic manners) claim to have proven NS.

mkarrmann, 11 hours ago