3 ms·
I mean, I guess that's the benefit of formal proofs? You don't need to "understand" it to know that it's true. Just going line-by-line and if checks out you are
by Pet_Ant 2y ago
I mean, I guess that's the benefit of formal proofs? You don't need to "understand" it to know that it's true. Just going line-by-line and if checks out you are good. The notion of "understanding" gets the "shut up and calculate" thrown at it.
- auntienomen 2y agoThis is a 5 paper long argument aimed at other mathematicians. It's a formal proof in the sense that it's standard math talk, but not a formally verifiable proof that could be, e.g., machine checked.
- p1esk 2y agoIt’s aimed at maybe a few hundred people in the world who can understand it. Maybe even few dozen.
- qsort 2y agoVery few proofs in actual professional mathematics are written in a formal proof structure where what you suggest is actually possible. You definitely need to understand the underlying ideas to follow along. "rewrite in lean when" isn't really practical (at least yet).
- lupire 2y agoThat's the flaw in formal proofs, not the benefit.
- gjm11 2y agoThe point of a proof is very much not just that it enables you to know that the thing is true, but also to give insight into why it's true. (And hence, e.g., what other related things are likely to be true and how one might prove them.) A 100% incomprehensible proof gives no such insight; a merely-somewhat-incomprehensible proof gives less insight than a more comprehensible proof could.