alt Hacker NewsAside from the usual squabbling about AI, it seems the bombshell claim is this:
"In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations."
So these authors seem to be claiming that OpenAI has not really proven Navier-Stokes at all. If I get their idea correctly, they are claiming that the LLM has not formalized the original "natural language" idea of Navier-Stokes correctly. If true, it would mean that their purported Lean proof is not actually a proof of Navier-Stokes at all, but something that is an incorrect translation of the original natural language idea. If correct, this is a really bold claim and I would like to see if other researchers agree.
Replies
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.
I read them as making a much weaker claim than this: not that the Lean proof isn't valid, just that it is not actually a formalization of the natural-language proof in the PDF they provided alongside it. I haven't heard any PDE people claim that the Lean proof is invalid, and I have heard things from a lot of them that imply that they think it is valid. (I'm a former research mathematician, but this is very far from my specialty, so I'm not really equipped to evaluate this claim myself.)
The claim is about the equivalence between two proofs and says nothing about the correctness of either proof. This seems to be confusing a lot of people.
> has not formalized the original "natural language" idea of Navier-Stokes incorrectly
Did you mean “not…correctly”?
Nobody has proven or disproven NS equations.
NS is continuous approximation to what is otherwise a discrete system. Particle collisions are discrete time events that are averaged over time. NS loses accuracy for very, very, very very low fluid densities and energies.
AI "proving" that this approximation can numerically "blow" up does not mean the approximation loses validity.
[dead]
No, they're not claiming that.
No one is disputing that the Lean formaization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.
The authors are claiming that the Lean proof is not the same proof as the NL one. Therefore, we shouldn't yet have confidence that the NL proof is valid.
This is an important claim which the math community will need to work through. However, the Lean proof alone is sufficient for OpenAI to (reasonably confidently, leaving aside questions of academic manners) claim to have proven NS.