University of Cambridge > > Microsoft Research Cambridge, public talks > Microsoft Distinguished Research Lecture: What are the Prospects for Automatic Theorem Proving?

Microsoft Distinguished Research Lecture: What are the Prospects for Automatic Theorem Proving?

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact msrcenq.

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.

Please register for this talk to ensure your place:

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2019, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity