Machine Learning for Theorem Proving

The course on learning problems in theorem proving introduces the design of automated and interactive theorem proving systems as well as proof certifiers and discusses the various machine learning problems that correspond to the built in heuristics. First, the course will focus on the high-level learning problems in proof assistants and techniques for the selection of relevant lemmas in large libraries. Next the focus of the course will be on strategy selection and strategy tuning using learning. Finally internal guidance of automated reasoning systems, including prediction of useful inference steps and tactics, as well as the evaluation of intermediate proof states will be discussed. Registration for the exams is mandatory, 5-2 weeks before the exam!