Abstract

Much of the mathematics education literature at the university level is concerned with the difficulties that first year undergraduate students encounter with proof and proving. The difficulties are mainly due to problematic use of formal language and lack of identification of the main mathematical concepts involved in a proof. Educators and mathematicians have devised several teaching interventions aimed at facilitating the learning of proof, including the use of computer-based theorem provers. In this talk we will present findings from a project that investigated the impact of students’ engagement with the automated thereon prover Lean (https://leanprover.github.io) on their subsequent ability to construct valid proofs.

Bios

Paola Iannone is Senior Lecturer in Mathematics Education in the Mathematics Education Centre at Loughborough University. Her research focuses on mathematical reasoning and the summative assessment of mathematics at university. She is presently investigating the potential of using the automated theorem prover Lean to teach first year mathematics students.

Athina Thoma is Lecturer in Mathematics Education at the University of Southampton Education School. Her current research interests include the impact of programming on mathematics undergraduate students’ learning, transition between secondary school and university mathematics, and teaching proof with the automated theorem prover Lean.