Deep Learning in Interactive Theorem Proving - IPAM at UCLA

Explore deep learning applications in interactive theorem proving through this 55-minute conference talk by Jason Rute of IBM at IPAM's Machine Assisted Proofs Workshop. Delve into past progress, future possibilities, and major challenges in applying machine learning to formal mathematics. Examine key topics including data availability, tool effectiveness, data gathering, representation, grammar, premise selection, term generation, next move prediction, reinforcement learning, expert iteration, and expertise. Address critical issues such as data contamination and benchmarking strategies while considering the broader implications of AI in theorem proving. Gain valuable insights into the intersection of deep learning and interactive theorem proving, and understand how these challenges connect to the wider field of machine learning.

Intro
About this talk
Challenges of IPAM
Is there enough data
Tools
Do they work
Gathering data
Representation
Grammar
Premise Selection
Term Generation
Predict the Next Move
Reinforcement Learning
Expert iteration
Expertise
Other stuff
Challenges
Data Contamination
Benchmarking strategies
AI and theorem proving