Abstract

Our SSHRC-funded research project aims to investigate the use of interactive theorem provers at the undergraduate level with a view to assessing their implications. Our hypothesis is that a proof assistant could be a useful additional tool in teaching undergraduate mathematics, with the potential to foster mathematical understanding and in particular students’ competence in proving. In this talk, we will share preliminary research findings on the introduction of the Lean theorem prover to undergraduate students, student interviews we have conducted, and instructors’ insights and suggestions stemming from their teaching experience of using Lean.

Bio

Gila Hanna is a Professor Emeritus at OISE, University of Toronto. Her research interests include the role of proof in mathematics education, philosophical aspects of proof, and proof technology.

Kitty Yan is a Postdoc Fellow at OISE, University of Toronto. Her research interests include students’ learning and understanding of mathematical reasoning and proof, mathematical content knowledge of prospective teachers, and use and integration of digital technology to enhance concept development.