Mathematical definitions, formally speaking

This talk will give an introduction to my current project, which aims to write all the theorems and definitions of mathematics in a computer-readable form.   By "computer-readable", we mean much more than TeX, Maple, or Sage.  We mean that the math is expressed in terms of the rules of logic and foundations of mathematics. This project is expected eventually to encompass all branches of mathematics.