Abstract
It is very tempting, as a mathematician, to use Lean to try and check some of your own proofs, especially when you're unsure of them. The obvious problem with that is that no paper proof is as detailed as a formalized proof, but this is not the only pitfall. I will talk about some of the other problems one might encounter.