Abstract

In my article on proof [Philosophia Mathematica (3) 5 (1997), 153—165], I suggested or intimated that computer proofs of mathematical theorems had been found only for relatively simple or trivial theorems. I am obligated to Martin Davis and R. S. Boyer for the information that this suggestion or intimation is incorrect. For instance, a machine proof of quadratic reciprocity was published by D. M. Russinoff in J. Automated Reasoning 8 (1992), 3–21. A machine proof of the unsolvability of the halting problem has been published by R S. Boyer and J. S. Moore. This and many other examples are presented in Chapter 1 of their book, A Computational Logic Handbook, Academic Press, 1990. A second edition of this book is expected shortly