Recorded 16 February 2023. Jason Rute of IBM presents "Deep learning in interactive theorem proving" at IPAM's Machine Assisted Proofs Workshop. Abstract: Deep learning has made progress in many diverse areas, often leveraging a relatively small toolbox of powerful techniques. One promising area of application is formal mathematics and interactive theorem proving. I will talk about past progress and future possibilities, focusing on the big picture. I will also talk about the many challenges and how they connect to challenges in machine learning as a whole. Learn more online at: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/