Abstract

It has become difficult to think about a future for mathematics research that does not include Interactive theorem provers (ITPs) and ITPs are entering the classroom everywhere. The list of courses using Lean, one such ITP ,  on the Lean community page includes – at the time of writing this abstract – 49 courses. These are both ‘transition to proof’ type courses and more advanced course for finalists and postgraduate students.   In this talk I will map  current (educational) research on the use of Lean for teaching and, in order to do so, I will first discuss some findings from educational studies on the impact of using Lean as part of ‘introduction to proof’ courses in first year university mathematics. I will particularly  focus on what research can tell us about the interaction between human (student) and tool (Lean). I will  then draw some conclusions on the affordances and drawbacks of using Lean  to support students’ transition to university mathematics and indicate some directions for future research.