While coq is an automated theorem prover, I've had a tremendous amount of fun working my way through Software Foundations[1]. The vast majority of the proofs are assembled "by hand", but with coq verifying steps. For someone like me who has a "late in life" fascination with mathematics, doing proofs using coq has been fantastic.

[1] https://softwarefoundations.cis.upenn.edu/