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.