Students’ engagement with Lean: working in the Advanced Proposition World of the Natural Number Game

Part of the "Learning Mathematics with Lean-2nd Event" sites.google.c...
Title: Students’ engagement with Lean: working in the Advanced Proposition World of the Natural Number Game
Speakers: Dr Paola Iannone & Dr Athina Thoma
Abstract: In this talk, we report on the different ways in which two first-year students engaged with level 4 of the Advanced Proposition World in the Natural Numbers Game. During the interviews, which were video recorded, students shared their screens and used the think aloud protocol while programming in Lean. Here, we analysed the proofs they produces in Lean, we report on their comments on the proofs while they produced them and we highlight the differences between the ways in which the two students think about programming the Lean proofs and the role that they ascribe to the ITP. We conclude with some implication for the use of Lean in undergraduate mathematics teaching.