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.