I will speak about the use of the interactive theorem prover Lean to teach proof and introductory pure mathematics to undergraduate mathematics students, with a focus on my experiences and observations at a UK university. The talk discusses the challenges common to new students, how Lean can help by clarifying the notion of proof and giving students instant feedback. I will address the difficulties involved in teaching with Lean.