I'm learning lean with that intent (to self learn mathematics). I get distracted trying to learn how to do better proof automation and tactic golf.

Also, since I don't see anyone mentioning so it far: there is a currently fairly active Zulip chat for the lean prover. They have been quite helpful for me getting started.