Comment by fasterik
6 hours ago
As far as I understand it, nobody is disputing the correctness of the Lean proof, or that it proves the conjecture it actually claims to prove. That's sufficient to consider the problem "solved". The natural language proof is a "nice to have".
The claim in TFA is that the formalization(in Lean) of the problem does not correspond to the natural language statement of the problem, such that the statement proven is not the conjecture for which proof is required for the problem to be considered "solved".
>the statement proven is not the conjecture for which proof is required for the problem to be considered "solved".
that's not the claim. the formal statement of the problem for the NS proof was written by humans not autoformalized.
That's not the claim made in TFA. See the sibling comments, in particular about the DeepMind formalization.
[flagged]
Please make your substantive points without swipes. This is in the site guidelines: https://news.ycombinator.com/newsguidelines.html.
Does that contradict what I said? In that quote, it says that the NL proof does not correspond to the Lean proof. However, the statement of the theorem in Lean is independent from the NL proof. It comes from a DeepMind repository, which as far as I'm aware has been accepted by the community as a valid formalization of the original Clay Institute statement.
https://github.com/google-deepmind/formal-conjectures/blob/8...
[dead]
Both proofs may be correct, and the problem may indeed be solved. My point is that it should not be assumed.
> Maybe read the original article before replying, at a minimum.
Maybe read the comment before replying, at a minimum.