Hands on with Lean

GQT School — Woudschoten, August 2022

Abstract. Lean is a proof assistant, a piece of software that understands mathematical definition, theorems, and proofs. It has been used to formally verify some high-profile results, including a foundational theorem of Scholze and Clausen in condensed mathematics.

Mathlib is the main mathematical library for Lean. It contains the definition of groups, rings, fields, topological spaces, manifolds, Lie algebras, and much more.

This workshop will focus on getting hands-on experience with Lean. There will be two talks explaining background material and giving an overview of the state of the art.


A laptop with ≥ 8GB RAM will be useful.

Lean can run in your browser, but a native installation is much faster. During the GQT School there will be time to install Lean, but feel free to install it beforehand and give a shot at some of the resources below.