We give an introduction into the history of proof assistants, recent formalization projects, and describe typical challenges when formalizing mathematics.
We demonstrate how to use prove theorems in Lean, in the process learning the most common tactics and how to write idiomatic Lean code.
Before the seminar, we will assist in installing Lean and mathlib from 2.30pm in Room 107 Greg Hjorth.Machine learning for theorem proving has classically focused on lemma selection and guidance of automated reasoning processes, where statistical methods help navigate large formal libraries and search spaces. More recent work has expanded this perspective toward coming up with useful conjectures or even theory exploration, refocusing the attention from supervised tasks on given statements to proposing useful new ones. In the second half of the talk I will turn to our most recent results on automating large parts of the formalization process, combining modern LLMs with proof automation. I will discuss the direct use of multiple collaborating LLMs, providing them with effective formalization incentives, and ways such approaches can be supervised towards a particular mathematical goal.