Working with Coq and trying to understand and use it has been a good brain stretcher for me. It's solidified my understanding of proofs to prove a bunch of simple number theory things in it, as well as creating my own types and experimenting with them.

It's a bit above my academic pay grade, so reading the documentation is always daunting, but I understand the basics. Still can't figure out how to use the notation system.