BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Microsoft Distinguished Research Lecture: What are the Prospects f
 or Automatic Theorem Proving? - Prof Sir Timothy Gowers
DTSTART:20151001T153000Z
DTEND:20151001T163000Z
UID:TALK60619@talks.cam.ac.uk
CONTACT:41807
DESCRIPTION:For several decades people have tried to write computer progra
 ms that can find proofs of mathematical statements. There have been some n
 otable successes\, such as a computer-discovered proof of the Robbins conj
 ecture\, which had previously been an open problem. But in general\, progr
 ess has been disappointing: many problems that are well within the reach o
 f an averagely good undergraduate are way beyond what the best programs ca
 n manage\, and for a certain class of problems we seem to have reached an 
 impasse.\n\nThere are two main approaches to automatic theorem proving: th
 e human-oriented approach\, which tries to get a computer to mimic as clos
 ely 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 machin
 e-oriented approach is more fashionable\, but I shall argue that to get be
 yond the impasse it will be essential to return to the human-oriented appr
 oach. I shall describe some preliminary work that I have done with Mohan G
 anesalingam\, and speculate about how one might go about programming a com
 puter to solve problems that for the moment cannot be solved without human
  ingenuity.\n\nPlease register for this talk to ensure your place: http://
 research.microsoft.com/en-us/events/msdrl/wpatp.aspx
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR