Jason Rute - Deep learning in interactive theorem proving - IPAM at UCLA

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: www.ipam.ucla.edu/programs/wor...