J. McCarthy

We envisage the use of computer proof-checking in mathematics as follow: The mathematician already has formalizations of this branch of mathematics and the computer system has stored in it the theorems that have previously been proved. In addition, there are a number of techniques embodied in programs for generating proofs. The mathematician expresses his ideas of how a proof may be found by combining these techniques into a program. The computer carries out the program which may prove the theorem, may generate information that will guide another try, may indicate an elementary misconception, or may be of no help whatsoever.

Back to the Nature of the PRL Project main page.