BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Towards a database of motivated proofs - William Timothy Gowers (U
 niversity of Cambridge)
DTSTART:20260331T090000Z
DTEND:20260331T100000Z
UID:TALK245707@talks.cam.ac.uk
DESCRIPTION:By a&nbsp\;motivated proof\, I mean a proof\, or more precisel
 y a presentation of a proof\, that makes transparent where the ideas come 
 from. Much mathematical literature is not motivated in this sense: it is f
 ull of definitions and lemmas that appear to come out of nowhere and demon
 strate their utility only well after they are introduced. This is a proble
 m both for human mathematicians wanting to learn how to do research and fo
 r AI systems using mathematical literature as training data.&nbsp\;\nIn th
 is talk I shall describe a project\, funded by the AI-for-math fund of Ren
 aissance Philanthropies and XTX Markets\, to build a database of what we c
 all structured motivated proofs. A first step towards this goal is to crea
 te a platform that will encourage people to input proofs in the format we 
 are looking for. We have a working prototype of this\, mainly built by Ana
 nd Tadipatri\, a member of my group. It is very preliminary and lacks many
  features that we will need\, but it is at a stage where I can give a live
  demonstration of how to use it: this demonstration will occupy much of th
 e talk.&nbsp\;
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR