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?
replyThis is the formalization that was proven in Lean. As of now at least, it's believed to be a correct statement of the problem.
replyhttps://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.
replyand 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!
reply;)
deleted
replyIf 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.
reply