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.
