The paper does point out that we don't know if Astra stated the problem correctly in Lean.

There are a number of posts here that consider the correctness of the Lean code with high confidence. This paper I think weakens that confidence.

Generally I think we can agree we don't know if the NL proof is correct, or if the initial statement in Lean is correct. I suppose that's obvious.