But just to clarify: is either of them actually addressing the real Navier-Stokes, or will it turn out we'll end up with two pairs of proofs about something irrelevant to the actual problem?

This is the formalization that was proven in Lean. As of now at least, it's believed to be a correct statement of the problem.

https://github.com/google-deepmind/formal-conjectures/blob/8...

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.

Those are statements about auto-formalization and the NL proof. They're saying that further work needs to be done on verifying whether the Lean and NL proofs are equivalent, which is completely valid. But they're not disputing that the Lean formalization is a correct statement of the Millennium Prize problem. You can see in the link I provided (and the original pull request) that it was written by humans, reviewed by human experts, and is completely independent of the OpenAI effort.

Nobody is claiming they've misformalized Navier-Stokes.

They are claiming that the NL proof and the Lean proof are not consistent though: the NL proof is not being validated by the Lean proof, and the Lean proof is not being "explained" by the NL 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."

Yes, but that's irrelevant to what I said, which is that nobody is claiming they've misformalized Navier-Stokes itself.

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.

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

This has nothing to do with whether the lean proof certifies (the real) NS.

The proof is about one of a multitude of possible theorems you could prove about the Navier-Stokes equation. Nobody is claiming that the Navier-Stokes equation itself is misformalized. Rather, they are claiming that what the theorem they proved says about Navier-Stokes is misformalized, in the sense that it's a different theorem than the one informally proven in the natural-language proof.

But nobody is claiming that it's a theorem about a misformalization of the Navier-Stokes equation rather than about the Navier-Stokes equation itself, and nobody is claiming that the theorem they proved in L∃∀N isn't proven. Except random ignorant commenters on Hacker News.

I don't know why this is so difficult. It seems like a lot of commenters here have the reasoning ability of GPT-3, possibly because they're extremely drunk or sleep-deprived, or are actually GPT-3.

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

From computer science perspective the conclusion is obvious: untenable to have two representations without an exact translation or machine checked correspondence between then. All we have is a vibe translation using the LLM. The methodology should obviously be improved.

and clearly the computer science perspective is: get rid of the humans and express everything directly in lean so the computers can keep getting work done!

;)

If I understand well, they mean that the thing they proved in lean is not Navier Stokes. And they don't make any statement about whether the natural language proof is correct or not.