4 ms·
How did proof itself get so reliable? The process of convincing yourself that a proof is correct isn't so different from the process of convincing yourself tha
by panic 7y ago
How did proof itself get so reliable? The process of convincing yourself that a proof is correct isn't so different from the process of convincing yourself that a program is correct.
- hcs 7y agoAnd equivalently, if you had heavily-relied-on proofs that were as narrowly read and hard to follow as software, mathematics would be in just as bad a state.
- garmaine 7y agoYes, it is. This can be shown with theory: proving a program is correct is NP-hard, but verifying the proof is in P-space. It is way easier to show a proof is correct than to generate the proof in the first place.
- panic 7y agoTrue, at least for formal proofs. I was thinking more of traditional mathematical proofs, which are often as hard to formalize as programs are to prove correct. In both cases, convincing yourself that the proof or program is correct involves reading it and seeing whether each of its parts follows from or fits into the other parts to make a coherent whole. Of course, there are ways to fool the reader, but I think people learn to avoid writing in ways that are likely to mask errors (e.g., not reusing the same symbol to mean completely different things, both in proofs and in programs).