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.
If the reason for the differences was done intentionally in Lean (as opposed to hallucinate e.g. m+4 vs m+5 as mentioned in remark 3.2), then a simple recording of differences, and then afterwards pass back any changes to the original NL would fix the issue. If it was hallucinated, then there is no guarantee it wouldn't keep hallucinating, and thus you might never end up with the same proof no matter how many passes you do back and forth (see remark 3.4).
humans as a whole have always known the weakness of natural language is in its precision. In a way this isn't strange that this issue has come up.
These authors don't seem to be disputing that this Lean formalization of Navier-Stokes is correct. I don't think that gives us any new information about whether the generated Lean proof is or isn't a valid proof of this N-S blowup thing.
A proof of a theorem is different from the statement of the theorem. OpenAI has a Lean proof of the statement. That is all they need. There may be many different proofs of this statement, including NL proofs. It does not matter that these NL proofs may or may not be different from the Lean proof, at least for the correctness of the Lean proof. But of course the NL proof may be wrong. But who cares?
Indeed. If only some of those people would see the irony.
What matters most of all, as any first year student of mathematics would know, is whether the formal problem statement corresponds to the NL statement. TFA specifically states that at least some of the allegedly proven formal statements DO NOT.
Does the paper give a single example of one of the OpenAI solved theorems with a Lean certificate where the Lean statement does not correspond to the actual statement from the mathematical literature? I don't think so, but in case I am wrong, feel free to provide that example.
What OpenAI purports to have proven, as I understand it, is that certain initial conditions to that equation, plus "forcing" over time (which could be a literal force acting on the fluid such as stirring it with a spoon or some other extrinsic effect) only have finite (and therefore physically plausible) solutions for a finite period of time, after which singularities appear, with the velocity or pressure of some of the fluid approaching infinity as you approach the finite time limit.
This is a result that Terry Tao conjectured in 02014, but without the forcing: http://arxiv.org/abs/1402.0290
I think we can be pretty confident that the L∃∀N proof is really about Navier-Stokes. The question is whether what it says about Navier-Stokes is what we think it says.
https://github.com/google-deepmind/formal-conjectures/blob/8...
;)
Did you mean “not…correctly”?
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.