Schedule

08:45 - 09:15 | Self Registration

09:15 - 09:30 | Welcome

09:30 - 10:30 | Floris van Doorn - Mathematics in Lean

10:30 - 11:00 | Coffee Break

11:00 - 12:30 | Jeremy Avigad - Logic Foundations and Dependent Type Theory - Logic 

12:30 - 14:00 | Lunch Break

14:00 - 15:30| Alex Bentkamp - Automated Theorem Proving with Ordered Resolution and Superposition I

15:30 - 16:00 | Coffee Break

16:00 - 17:30 | Adam Zslot Wagner - Machine Learning and Theorem Proving I

09:00 - 10:30 | Jeremy Avigad - Logic, Foundations and Dependent Type Theory - Foundations

10:30 - 11:00 | Coffee Break and Group Photo

11:00 - 12:30 | Alex Bentkamp - Automated Theorem Proving with Ordered Resolution and Superposition II

12:30 - 14:00 | Lunch Break

14:00 - 15:30 | Floris van Doorn - Basics of Lean

15:30 - 16:00 | Coffee Break

16:00 - 17:30 | Floris van Doorn - Practice sessions in Lean: Basics and Computation

17:30 - 19:30 | Get Together with Drinks and Snacks 

09:00 - 10:30 | Jeremy Avigad - Logic, Foundations and Dependent Type Theory - Dependent Type Theory 

10:30 - 11:00 | Coffee Break

11:00 - 12:30 | Adam Zslot Wagner - Machine Learning and Theorem Proving II

afterwards          | Lunch break and free afternoon

09:00 - 10:30 | Floris van Doorn - Practice sessions in Lean: Sets, functions, logic I

10:30 - 11:00 | Coffee Break

11:00 - 12:30 | Floris van Doorn and Kyle Miller - Practice sessions in Lean: Sets, functions, logic II

12:30 - 14:00 | Lunch Break

14:00 - 15:30 | Alex Bentkamp - Automated Theorem Proving wit Ordered Resolution and Superposition III

15:30 - 16:00 | Coffee Break

16:00 - 17:30 | Floris van Doorn - Practice sessions in Lean: Topology

09:00 - 10:30 | Floris van Doorn and Kyle Miller - Practice sessions in Lean: Calculus

10:30 - 11:00 | Coffee Break

11:00 - 12:30 | Adam Zslot Wagner - Machine Learning and Theorem Proving III

12:30 - 14:00 | Lunch Break

14:00 - 15:30 | Open Session

afterwards         | closing