LFTCM 2020 Lean for the Curious Mathematician 2020

The workshop will take place from Monday 13th through Friday 17th July 2020.

All times mentioned below are in central European time (CEST, UTC+2:00).

The virtual “common room” for this workshop is the dedicated Zulip stream. In this stream we will post announcements, answer questions, and host any further discussion.

Most of the schedule below forms the beginner track of the workshop. Intermediate users can work on pair programming with more advanced users at any time, using the Zulip stream for coordination.

Recorded talks

The talks have been recorded, and are available in this Youtube playlist. The individual talks are also linked below.

Monday:

The goal of this first day is to make sure that all participants have Lean and its supporting tools installed, and to start proving things without knowing anything about foundations or theory building, using the Natural Number Game.

In parallel during the afternoon, intermediate users will have the opportunity to learn about Lean’s meta-programming framework, which allows to automate some proofs.

Time Activity Speaker
07:00 – 12:00 Tech support (installing Lean, using git + GitHub)  
13:00 – 13:30 Welcome + 1st Lean proof Scott Morrison
13:30 – 18:00 Natural number game (demo and exercises) Kevin Buzzard
13:30 – 18:00 Meta-programming and tactic writing Rob Lewis

Tuesday:

This second day focuses on basic proving techniques and manipulating elementary objects. It will mostly rely on the Mathematics in Lean tutorial. We will cover most of the content of the tutorial and help people doing the exercises.

Time Activity Speaker
10:00 – 12:00 Mathematics in Lean: basics (slides) Patrick Massot
13:00 – 15:00 Mathematics in Lean: logic Jeremy Avigad
15:00 – 16:30 Dealing with numbers: ℕ, ℤ, ℚ, ℝ, ℂ Rob Lewis
16:30 – 18:00 Dealing with sets and operations on them Jeremy Avigad

Wednesday:

This third day focuses on theory building. This includes defining mathematical structures (such as groups, rings, topological spaces…) and their relations as well as proving enough basic lemmas to make them usable. All the examples that will be discussed are already known to Lean, but we will explain how build them from scratch.

Time Activity Speaker
10:00 – 12:00 Structures and classes (video 1) (video 2) Floris van Doorn
13:00 – 15:00 Rebuilding an algebraic hierarchy Kevin Buzzard
15:00 – 17:00 Rebuilding a topological hierarchy Alex J. Best

Thursday:

This is the first of two days devoted to specific areas of mathlib, Lean’s mathematical library. Here we won’t rebuild definitions, but rather learn how built things can be used, mostly by reproving lemmas that are already in mathlib.

Time Activity Speaker
10:00 – 11:00 “Order”, including Galois connections Kevin Buzzard
11:00 – 12:00 “Groups, rings and fields” Johan Commelin
13:00 – 15:00 “Linear algebra” Anne Baanen
15:00 – 18:00 “Category theory” Scott Morrison

Friday:

This will be similar to Thursday, but focusing on topology, analysis, and differential geometry.

Time Activity Speaker
10:00 – 12:00 “Topology”, including filters (slides) Patrick Massot
13:00 – 15:30 “Calculus and integration” Yury Kudryashov
15:30 – 18:00 “Differential geometry” Sébastien Gouëzel and Heather Macbeth