All those who have marked first year students’ work will know that proof is one of the stumbling blocks for students in the transition to university mathematics. In this talk I will discuss some of the difficulties that students experience with proof.  I will then present the use of interactive theorem provers to teach transition to proof courses, some implementations and their affordances and drawbacks in terms of students’ learning. I will end this talk with  some future directions for research in the area.