Teaching undergraduates to construct mathematical proofs has always been a challenge. The advent of proof-assisting software such as Lean offers an opportunity to make the teaching of proof both more efficient and more effective. But what are the implications for pedagogy? To reap the potential benefits of the new technology, do we need a new and different set of instructional techniques? Based on initial experience using Lean with undergraduates and high-school students, this paper sets out what we see as some potential benefits (for both learners and teachers) of using Lean in the classroom, as well as our view of the changes in pedagogy that may be required.