balaclava9

No one is claiming it is proven in lean or in natural language. The Clay Institute, for example, has not said it’s proven.

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.

They are claiming that we do not know if Astra formalized all the elements of the Navier-Stokes proof in Lean correctly.

The Clay Mathematics Institute has not yet accepted the proof.

Yes it could be that neither the NL proof nor the Lean proof correspond to the actual Navier Stokes problem. Here's a quote from the paper--

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

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.

You may be overconfident here. The NL paper may be properly stating the Navier Stokes problem, and the Lean code may not be.

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.

The statement written in Lean, is not actually a correct description of the Navier-Stokes problem. It's some other easier statement. That's why the Lean code may not be a proof.

Here's a quote 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."

"Tracing the proof of (3.3) we find that the series arises from applying the Lean theorem coefficient_seminorm_bound, just as Figure 3 mentions. Consequently, the Lean results discussed in this section are weaker than (3.1) in the NL proof."

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?

Here is their remark.

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

My understanding is that the statements in the Lean proof might not actually correspond to the Navier-Stokes problem. And that requires mathematical insight to be able to verify, which could take quite a while.

fascinating story. amazing how people want to believe in the AI savior.

It’s nice to hear someone using English correctly.

Who is the lead writer of this paper? According to google Ziyi Zhang is a famous Chinese actress.

yeah i think that's an important point that this article should have mentioned:

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.

Nexus 6