3 ms·
I don't get the point about trivial proofs. Can't you just tell Lean to assume something is true and then get on with the rest of the interesting part?
by anonymousDan 1y ago
I don't get the point about trivial proofs. Can't you just tell Lean to assume something is true and then get on with the rest of the interesting part?
- jojomodding 1y agoYou can but that ruins the fun and also misses the point. How do you know your "trivial" theorem is actually trivial? Proofs are mechanized to increase our trust into them, and it defeats the point if you have to still manually review a myriad of helper lemmas.
- anonymousDan 1y agoYeah I guess it's more a question of methodology for me. You have several parts of a proof, and your intuition guides you that certain parts are more likely to be risky than others. Better to get those straight first since you've a higher chance of failure (potentially rendering much of the work you have already done pointless). Then you can come back to flesh out the hopefully more straightforward parts. This is as opposed to taking a purely bottom-up approach. At least that's how I often tackle a complex coding problem - I am no mathematician!