HEGL Community Seminar WiSe 2024-2025

The Seminar takes place on Mondays at 14:15, usually in Seminar Room C of the Mathematikon.

Schedule

04.11.2024

Speaker: Gihan Marasingha (University of Exeter)

Title: Teaching proof to new undergraduates with the Lean interactive theorem prover
Time: 14:15

Abstract:

I will speak about the use of the interactive theorem prover Lean to teach proof and introductory pure mathematics to undergraduate mathematics students, with a focus on my experiences and observations at a UK university. The talk discusses the challenges common to new students, how Lean can help by clarifying the notion of proof and giving students instant feedback. I will address the difficulties involved in teaching with Lean.