Schedule

The workshop will start with registration on Monday, August 17 at 8:30 and end on August 21 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? Speaker: Johan Commelin	Lecture 1: Sets and logic	Lecture 3: Algebraic structures and typeclasses	Start of project phase	Projects
11:00 - 12:30	Natural Number Game	Exercises	Exercises and announcement of topics	Projects	Projects, preparation of presentations
12:30 - 14:00	Lunch	Lunch	Lunch	Lunch	Lunch
14:00 - 15:30	Natural Number Game	Lecture 2: 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