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 Theo

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/ https://leanprover-community.github.io/ 2. http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game... 3. https://leanprover.github.io/theorem_proving_in_lean/ https://leanprover.github.io/theorem_proving_in_lean/