3 ms·
How do you know that what is being proved in the lean code is the same as the millennium prize criteria though?
by krackers 25d ago
How do you know that what is being proved in the lean code is the same as the millennium prize criteria though?
- keel-control 25d 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.