Seminar series
Date
Tue, 04 Nov 2025
12:00
12:00
Location
L4
Speaker
Remy Degenne
Organisation
INRIA LILLE
This tutorial will be a hands-on introduction to proving theorems in Lean, using its mathematical library Mathlib. It will not assume any previous knowledge about formal theorem provers. We will discover the Lean language, learn how to read a statement and a proof, and learn the essential "tactics" one can use to prove theorems in Lean.
Participants should come with a computer, and it would be best if they could install Lean before the tutorial by following the instructions at https://lean-lang.org/install/ . The installation should be easy and takes only a few minutes.