Interactive and automated theorem proving

The moment when research mathematicians need to pay attention to progress in automated theorem proving is coming closer and closer! I've been writing a category theory library in Lean (a new interactive theorem proving language), with the goal of learning how to write effective and helpful automation. This project would involve learning about interactive theorem proving, learning how to program in Lean (previous experience with a strongly typed functional language, e.g. Haskell, would be very helpful), proving theorems in category theory in Lean, and possibly also helping create new tactics for automatically proving theorems in this context. (Required background: you should have seen the definition of a natural transformation, and done some programming, preferably in a strongly typed language.)