The workshop will start with registration on Monday, July 21 at 8:30 and end on July 25 at 14:30. On the first three days, we will have lectures and guided exercise sessions and on Thursday and Friday, participants will work on formalisation projects of their choice.
| Time | Monday | Tuesday | Wednesday | Thursday | Friday |
|---|---|---|---|---|---|
| 8:30 - 9:00 | Registration | ||||
| 9:00 - 10:30 | What is Formalisation of Mathematics? | Sets and logic | Algebraic structures and typeclasses | Start of project phase | Projects |
| 11:00 - 12:30 | Natural Number Game | Exercises | Exercises and announcement of project topics | Projects | Projects, preparation of presentations |
| 12:30 - 14:00 | Lunch | Lunch | Lunch | Lunch | Lunch |
| 14:00 - 15:30 | Natural Number Game | Real analysis and linear arithmetic | Hike | Dependent type theory vs. set theory and formalisation for education. | Project presentations |
| 16:00 - 17:30 | Install Lean | Exercises | Hike | Projects |
Speaker: Johan Commelin
We will learn how to manipulate identities of sets, how to prove simple logic statements and see why they are really two sides of the same coin.
Why is 1 / 0 well defined in Lean? How to prove a sequence converges? We learn the fundamentals
of real analysis and linear arithmetic in Lean.
We will look into how groups, rings or vector spaces can be formalised in Lean. We explain what type classes are and how they can be used to work with algebraic structures.
On Thursday we will have two talks of 45 minutes:
Speaker: Fernando Chu
Abstract: TBA
Speaker: Pim Otte
Abstract: TBA