5 ms·
Why is no one skeptical that the solution is correct? There's not a _single_ comment asking whether this proof is legit or not.
by simianwords 9d 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.
- keel-control 8d agothere is a proof in lean4 it's correct by construction
- krackers 8d agoHow do you know that what is being proved in the lean code is the same as the millennium prize criteria though?
- keel-control 8d agoyou 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.