Specific conclusions associated with individual proofs have already been presented in the precedings chapters. In this chapter, we state some general conclusions and advance some specific comments on the Boyer–Moore theorem prover.

The social process by which mathematical arguments are scrutinized and accepted or rejected remains important even with the introduction of mechanized proof checking. The paper [MLP79] that we have quoted above, argues that mathematical proofs are interesting to mathematicians and are therefore examined with great care by means of the social process. The authors contend that proofs of computer programs are unlikely to be of similar interest to the social process. They express skepticism as to whether machine-assisted verification of programs and proofs could ever be feasible or illuminating. Though these arguments carry considerable weight, they are founded on some serious misconceptions on the role of proofs, formal proofs, and of mechanical verification. Proofs are not a means to obtaining certitude. As Lakatos [Lak76, page 48] writes, “the virtue of a logical proof is not that it compels belief, but that it suggests doubts.” While formalism might not always serve as a mechanism for the discovery of proofs or counterexamples, it can be used to expose the weaknesses in an argument and to isolate the assumptions on which an argument rests. Formalism is also useful in observing (and mechanizing) patterns of proofs.