This repository contains exercises and supplementary materials for the Hanoi Lean 2019 workshop.
To get started, first make sure that Lean is installed and you have the update-mathlib
script (see install instructions here).
Open a terminal and run
git clone https://www.github.com/jesse-michael-han/hanoi-lean-2019
cd hanoi-lean-2019
leanpkg configure
update-mathlib
The exercises are in the /src
directory.
DAY 1 (introduction, basics) | DAY 2 (tactics, metaprogramming) | DAY 3 (mathlib, library-building) | DAY 4 (formal abstracts, formal blueprints) | |
---|---|---|---|---|
10:00-10:50 | Hales | Han | Lewis | Vajjha |
Formal Abstracts - A Vision | Tactics and automation | Typeclass inference in Lean | Documentation for formal abstracts | |
10:55-11:10 | Morning break | Morning break | Morning break | Morning break |
11:10-12:00 | Lewis | Vajjha | van Doorn | Mark Adams |
Introduction to Lean I | Introduction to metaprogramming | Introduction to mathlib | Organization of formal abstracts | |
(Chapters 6 and 1-3 of TPIL) | ||||
12:00 - 1:45 | Lunch | Lunch | Lunch | Lunch |
1:45-2:35 | Trung | Baek | van Doorn | Hales |
Introduction to Lean II | Writing tactics | Best practices for library-building | Formal abstracts - the way forward | |
(Chapters 5-8 of TPIL) | Suggested projects | |||
2:35-3:25 | Trung | Baek | van Doorn | Working groups (suggested projects) |
Group theory in Lean | omega | Exercise session | ||
3:25-3:40 | Afternoon break | Afternoon break | Afternoon break | Afternoon break |
3:40-4:30 | Exercises/working groups | Hanoi Lean Working Group | Exercises/working groups | Working groups (suggested projects) |
TBD | ||||