This project explores undergraduate students’ experiences when engaging with an Interactive Theorem Prover (Lean), by Dr Athina Thoma and Dr Paola Iannone.

The project began in 2018 where we explored the challenges and benefits of mathematics undergraduate students’ engagement with Lean. In that phase of the project we were interested in the impact that engagement with Lean had on students’ pen-and-paper proofs. Now, we are analysing data which focuses on students’ engagement with Lean and examines the different ways that students’ use the Interactive Theorem Prover.