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.