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

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

• Prof Sir Timothy Gowers
• Thursday 01 October 2015, 16:30-17:30
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

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: http://research.microsoft.com/en-us/events/msdrl/wpatp.aspx

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

This talk is included in these lists:

• All Talks (aka the CURE list)
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Featured talks
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• custom
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.