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