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.
Prerequisites
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.
Resources
- Community website.
Online entry point for everything Lean.
I will highlight the most important parts below.
- Zulip.
The chatroom for the Lean community.
All Lean-related questions are welcome.
Support around the clock.
- Natural number game.
An online tutorial.
A great way to take your first steps with Lean.
- Installation instructions.
For Linux, Mac, and Windows.
Note: There has been some trouble recently with installing Lean on the newest generation Macs.
If you have problems, please ask on Zulip.
- Tutorials.
A great next step after the Natural Number Game.
- LFTCM exercises.
Material from a week-long Lean workshop.
Pick any topic you are interested in.
Corresponding videos are available on
Youtube.
- HoTT book.
The first chapter is a great introduction to type theory for the working mathematician.
- Theorem proving in Lean.
An online book that explains all the nitty-gritty details of working with Lean.