What are the prospects for automatic theorem proving?
206For several decades people have tried to write computer programs that can find proofs of mathematical statements. There have been some notable successes, such as a computer-discovered proof of the Robbins conjecture, which had previously been an open problem. But in general, progress has been disappointing: many problems that are well within the reach of an averagely good undergraduate are way beyond what the best programs can manage, and for a certain class of problems we seem to have reached an impasse. There are two main approaches to automatic theorem proving: the human-oriented approach, which tries to get a computer to mimic as closely as possible the way that a human would find a proof, and the machine-oriented approach, which aims to surpass what humans can do by exploiting the vastly superior speed and memory of computers. Currently, the machine-oriented approach is more fashionable, but I shall argue that to get beyond the impasse it will be essential to return to the human-oriented approach. I shall describe some preliminary work that I have done with Mohan Ganesalingam, and speculate about how one might go about programming a computer to solve problems that for the moment cannot be solved without human ingenuity.