Computer theorem provers in the classroom?

Details

A computer theorem prover is a computer program which understands mathematical definitions, theorems and proofs, and can check proofs written in the language of the system to see if they are correct. Over the last few years I have been experimen4ng with the idea of getting mathematics undergraduates to do mathematics (for example, their problem sheets) using the Lean theorem prover. My initial vision of how this would work out turned out to be completely and utterly wrong. Moreover, the reasons I was initially motivated to do it are totally different from the reasons I continue to do it. I'll tell the story of where we are and where I think we're going.