← Back to context Comment by keel-control 16 hours ago there is a proof in lean4 it's correct by construction 2 comments keel-control Reply krackers 7 hours 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 3 hours ago 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.
krackers 7 hours 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 3 hours ago 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.
keel-control 3 hours ago 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.
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.