What are the prospects for automatic theorem proving?

Опубликовано 22 июня 2016, 20:17

For 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.