Comment by omnicognate
6 hours ago
If I understand the abstract correctly (big caveat), they aren't saying they didn't prove it. They're saying they gave two proofs, one in natural language and one in Lean, that are not equivalent to each other. I assume the main significance is that the Lean proof is not a formal verification of the natural language one and the natural language proof is not a readable explanation of the Lean one. Both of those things can be desirable, so to complete the set we'd get 4 proofs.
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...
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.