Comment by robinzfc
2 days ago
The purpose of math is indeed to increase our understanding, but the correctness of proofs is a precondition for that. A wrong proof does not increase understanding, although it may create such illusion. Proof assistants provide scalability to correctness checking and this way they contribute to understanding.
Some proof assistants contribute more directly to understanding by making proofs easier to study.
Indeed. Strange that the previous commenter attacked such an obvious strawman ... they responded to my statement about the purpose of proof with a statement about the purpose of math, which I hadn't mentioned. Also strange is the claim that the purpose of a proof is to show "why" a statement is true rather than that a statement is true. Some proofs help understand the "why" but many don't (proofs of the FLT included) and informal discussion is usually better for that, and is often why we believe that an unproven proposition is true -- e.g., it's widely believed, for good reasons, that P != NP, but no one knows how to prove it. Ditto for the Collatz conjecture.