BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:What role is there\, if any\, for human-oriented automatic theorem
  proving today? - William Timothy Gowers (University of Cambridge)
DTSTART:20250613T081500Z
DTEND:20250613T091500Z
UID:TALK230653@talks.cam.ac.uk
DESCRIPTION:Human-oriented theorem proving is the approach to automatic th
 eorem proving that seeks to create algorithms that find proofs in a way th
 at is modelled as closely as possible on how humans find them. It used to 
 be contrasted with machine-oriented theorem proving\, where the emphasis w
 as far more on exploiting to the full the vastly superior speed and memory
  of computers. At the last Big Proof meeting I argued that despite the fac
 t that the machine-oriented approach was more fashionable\, it was importa
 nt not to lose sight of the human-oriented approach. Since that meeting\, 
 the whole discussion has been greatly changed by the dramatic developments
  in AI. I shall argue\, but more tentatively\, that it is still worth inve
 sting significant effort into understanding how human mathematicians find 
 proofs. I shall also report on some of the work my group in Cambridge has 
 been doing in that direction.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR