The claim is about the equivalence between two proofs and says nothing about the correctness of either proof. This seems to be confusing a lot of people.
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.
Is it obvious? The formal statement that Astra proved was written by a human, submitted to a DeepMind repository, and reviewed by human experts in a pull request. It's completely independent of OpenAI's effort. No expert in PDEs or formal verification has disputed it as far as I'm aware.
https://github.com/google-deepmind/formal-conjectures/blob/8...