There is a Kevin Buzzard's course on «Formalizing Mathematics» available on GitHub of Imperial College London. It is structured as workshops in Lean. I started it to pass time during my vacation. Enjoying it very much so far. Proving theorems seems to be the perfect fit to learn the language hands.