The Seminar takes place on Wednesdays at 14:15, usually in Seminar Room A of the Mathematikon.
Schedule
21.05.2025
Speaker: Athina Thoma (University of Southampton).
Title: Teaching mathematics using Lean: Insights from students and lecturers.
Time: 14:15.
Abstract:
Interactive Theorem Provers (ITPs) like Lean are increasingly being used in university mathematics teaching, either as core components of courses or as optional enrichment opportunities. This talk presents findings from educational research exploring how students experience and engage with Lean when first introduced to it. Drawing on data from students’ pen-and-paper proof writing, questionnaire responses, and interviews, I will discuss challenges students encounter and the affordances Lean offers. Complementing the student perspective, I will also share insights from lecturers who integrated Lean into an introductory proof course, highlighting how they adapted their teaching approaches. Together, these perspectives provide insights on the pedagogical opportunities and limitations of using Lean to teach mathematics.
