Interactive Theorem Proving in Education and Research

Timetable

24 July 2024 // University of Exeter // Online

All times are in British Standard Time (UTC+1)

TimeSpeakerEvent
09:30Introductory Lean workshop:
Lean via the Game Engine
10:30Coffee break / Registration
11:00Athina ThomaLearning Lean: Exploring students’ perspectives and use of Lean
11:30Patrick MassotTeaching using a proof assistant and controlled natural language
12:00Questions
12:15Kevin BuzzardThe state of the art in the formalisation of research-level mathematics
12:45Heather MacbethA “calculation-heavy” introduction to proof, with support from Lean
13:15Questions
13:30Lunch
Student posters
14:15Jeremy AvigadTeaching with Lean
14:45Achim Brucker
Diego Marmsoler
Introducing Isabelle to students with little maths or theoretical computer science background
15:15Questions
15:30Workshop:
Mathematics in Lean
17:00Close