5 ms·
there is a proof in lean4 it's correct by construction
by keel-control 9d ago
there is a proof in lean4 it's correct by construction
- krackers 9d 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.