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.
The talks have been recorded, and are available in this Youtube playlist. The individual talks are also linked below.
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 |
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 |
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 |
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 |
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 |