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 (KBG 208) | ||||
| 9:00 - 10:30 | What is Formalisation of Mathematics? (KBG 208) | Sets and logic (KBG 208) | Algebraic structures and typeclasses (KBG 208) | 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 proof assistants for education. | Project presentations |
| 16:00 - 17:30 | Install Lean | Exercises | Hike | Projects |
The summerschool will take place in Victor J. Koningsbergergebouw (KBG). We will use rooms KBG 208 and KBG 224.
Speaker: Johan Commelin (Slides)
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: In this talk, we briefly recall the history of set theory and type theory and ponder about an important, but often ignored, question: what is a set? Once this is understood, then the analogous question for types has an easy answer. We then proceed to compare set theory and type theory, both in theoretical aspects (such as consistency) and in practical aspects (such as usability). In view of this comparison, we explain why Lean uses type theory, instead of set theory.
Speaker: Pim Otte
Abstract:The key skill for a mathematician is being able to write down proofs of theorems. Proof assistants can check Waterproof is an educational software tool that aims to teach this skill to mathematics students, built on top of the Rocq theorem prover. The goal of this tool is to provide students with an environment that gives immediate feedback, while resulting in a proof that would also be accepted on paper. In this talk I will demonstrate the Waterproof tool, discuss the practical learnings from applying this in teaching at the Technical University of Eindhoven and showcase Verbose Lean, which achieves a lot of the aims of Waterproof in Lean.