Comment by simianwords
17 hours ago
Why is no one skeptical that the solution is correct? There's not a _single_ comment asking whether this proof is legit or not.
17 hours ago
Why is no one skeptical that the solution is correct? There's not a _single_ comment asking whether this proof is legit or not.
there is a proof in lean4 it's correct by construction
How do you know that what is being proved in the lean code is the same as the millennium prize criteria though?
you can get another LLM to verify / if the lean doesn't have `sorry` used to skip certain parts of the proof etc. It's much easier once it's in lean4 because checks like that can be done computationally.