Each of the following tutorials is available in an online version that runs alongside a Lean in your browser, and as a PDF document. The most comprehensive is the following:
- Theorem Proving in Lean
A introduction to using Lean as an interactive theorem prover.
online tutorial, pdf
The next two are incomplete and not fully up to date, but may still be helpful:
Reference (work in progress)
The current version of Lean is Lean 3, and is under active development. The source code and libraries can be found on github.
The previous version of Lean, Lean 2, is still being maintained but not developed. Lean 2 has special support for homotopy type theory and a substantial library. The source code and libraries can be found on github.
A public chat room dedicated to Lean is open on Gitter.
You are welcome to join the Lean user forum on Google Groups.