Integrating Formal and Informal Reasoning

RSVP here: https://forms.gle/b4hXBEVJuPtB3z157 

ML models for automated theorem proving are usually trained to output entire proofs as text in the Lean proof assistant. With a little ingenuity, we can devise a better interface that is significantly easier, plays to the strengths of ML, and reveals the structure of mathematics. In this talk, I will share my learnings from a few years of investigation into building future-proof infrastructure for automated theorem proving, as it relates to learning-based methods.