Are you a mathematician who wants to get started? Try the natural number game. Finished that? Try maths challenges for the Lean curious or other things mentioned in the natural number game FAQ.
The Lean Prover Community website has a bunch of interesting stuff, including explanations on how to install Lean, documentation for mathlib, and other ways to start learning Lean.
I learnt a lot from Theorem Proving In Lean and I’m slowly helping to write Mathematics in Lean.
Xena 