balaclava9
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.
"In all cases the correctness of the formal proof does not say anything about the correctness of the NL proof."
The Clay Mathematics Institute has not yet accepted the proof as it takes a while to review.
"The Clay Mathematics Institute is dedicated to furthering the beauty, power and universality of mathematical thought. Curating the Millennium Prize Problems is one of the most important ways in which it pursues this goal. The rules governing the prizes describe the process for evaluating what has been achieved and for assigning credit. The process is deliberately unhurried, but we will provide updates."
https://www.claymath.org/news/navier-stokes-announcement/
We can see therefore that we don't know if the OpenAI program wrote the NL statement or proof correctly. Or if maybe it needs work. Or if maybe it has significant errors.
We also don't know if Astra properly wrote the initial statement of Navier-Stokes correctly in Lean.
The Clay Mathematics Institute has not yet accepted the proof.
"Remark 3.4 (Further potential mistranslations of the Navier-Stokes proof). The above examples require careful manual checking of both the NL proof as well as the Lean proof, which is delicate and highly time consuming. Moreover, the fact that we display only two examples does not mean that these are the only cases of mistranslations."
"3.1. When the NL paper declares stronger statements than what Lean proves
We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement."
It seems the Lean version may not be a correct statement of the Navier-Stokes problem.
They go on to say this--
Remark 3.4 (Further potential mistranslations of the Navier-Stokes proof). The above examples require careful manual checking of both the NL proof as well as the Lean proof, which is delicate and highly time consuming. Moreover, the fact that we display only two examples does not mean that these are the only cases of mistranslations.
Here's from the paper--
3.1. When the NL paper declares stronger statements than what Lean proves
We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement.
Here's a quote from the paper. "In the following example the AI autoformalisation results in a different Lean proof of a weaker statement."
So the question is, was the Navier-Stokes problem framed properly in the lean code, or is some easier problem represented in the Lean code?
rather than a company trying to embarrass the government for asking, it's the government trying to embarrass a company for not complying! -- the opposite situation from what's addressed by the UK Law.