[monkeyelite]

> The purpose of a proof of an assertion is to demonstrate that the assertion is true. Once that is done, the assertion can be treated as a theorem and other results can be built upon it.

No. The purpose of math is to increase our understanding, not check off boxes.

In your model you might as well have a computer brute force generate logical statements and study those. Why would that be less valuable then an understanding of differential equations?

[robinzfc]

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.

[jibal]

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.