Master Praktikum: Formalization in Lean

Instructor: Xavier Généreux

Content

The Lean Theorem Prover is a functional programming language that double as an interactive theorem prover (ITP). In this Praktikum we will explore how to formalize algorithms and mathematical theorems.