To put it in code terms.

1) The code and the comments disagree.

2) The code passes the tests.

3) The comments promise functionality the code does not implement.

The first post was "It doesn't meet the business requirements the comments indicated, so the software is broken." The replying post was "Actually, the business requirements were faithfully turned into tests, so the software is fine. The comments need to be rewritten"

Also an outsider to the field and wondering the same thing. I can't see the difference. Can someone explain please?

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."

The English language description doesn't do the same thing as the code the AI wrote.

This doesn't answer the question. The question was: what was the difference in A and B. Your answer looks like this:

A: The English language description doesn't do the same thing as the code the AI wrote.

B: The English language description doesn't do the same thing as the code the AI wrote.

A and B are the same; there is no difference. Is this what you meant? Or did you mean the opposite of this? If you meant the opposite of this, what exactly is the difference?

ie the code had bugs, and they didn't update the documentation. wouldn't be the first time.