The Lean Community website [1] is a great place to start. Depending on your background you might like to dive right into the Natural Number Game [2] or the Theorem Proving in Lean [3] (both linked from the Community site).

1. https://leanprover-community.github.io/

2. http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game...

3. https://leanprover.github.io/theorem_proving_in_lean/

See the resources over at https://leanprover-community.github.io/learn.html and the youtube playlist of the Lean for the Curious Mathematician workshop: https://www.youtube.com/playlist?list=PLlF-CfQhukNlxexiNJErG...

An addictive personality :).

Theorem proving can be a fun open-world videogame, and I do hope these aspects can be refined overtime to make real mathematics a lot more accessible.