They published both a natural language proof and a lean proof. This paper says the NL proof does not match does not match the lean proof, using different arguments and some stronger claims. It does not claim the lean formulation of NS or the rest of the lean proof is invalid.

"The Lean code merely tells us that the theorem is correct, yet the NL proof with intermediate arguments, lemmas and results may be incorrect or have incorrect arguments."

You didn't answer the question. Quoting from upthread:

A: "In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations."

B: "No, they're not claiming that [...] The authors are claiming that the Lean proof is not the same proof as the NL one"

The question was: what's the difference between A and B?

Your answer to that question was "This paper says the NL proof does not match does not match the lean proof".

It seems to me like A is the exact same thing as B, and you are here claiming that they're different things while merely repeating the same claim that was already claimed in both A and B.

Statement A is upthread quoting the paper, and is not the statement B is arguing against. B is arguing against the incorrect statement "So these authors seem to be claiming that OpenAI has not really proven Navier-Stokes at all."