By a motivated proof, I mean a proof, or more precisely a presentation of a proof, that makes transparent where the ideas come from. Much mathematical literature is not motivated in this sense: it is full of definitions and lemmas that appear to come out of nowhere and demonstrate their utility only well after they are introduced. This is a problem both for human mathematicians wanting to learn how to do research and for AI systems using mathematical literature as training data.
In this talk I shall describe a project, funded by the AI-for-math fund of Renaissance Philanthropies and XTX Markets, to build a database of what we call structured motivated proofs. A first step towards this goal is to create 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 Anand 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 the talk.
