There are many ways to start learning Lean, depending on your background and taste. They are all fun and rewarding, but also difficult and occasionally frustrating. Proof assistants are still difficult to use, and you cannot expect to become proficient after one afternoon of learning.
Whatever your background, if you want to dive right away, you can play the Natural Number Game by Kevin Buzzard and Mohammad Pedramfar. This is a online interactive tutorial to Lean focused on proving properties of the elementary operations on natural numbers.
For a faster paced and broader dive, you can get the tutorials project. (You already have it if you installed an autonomous bundle or followed the instructions on this page.) This tutorial is specifically geared towards mathematics rather than computer science. The last files of this project are easier if you have already encountered the definition of limits of sequences of real numbers.
A brand new resource that is still under construction is Mathematics in Lean. It can be read online, or downloaded as a pdf, but it is really meant to be used in VSCode, doing exercises on the fly (see the instructions). It currently covers roughly the same ground as the tutorials prooject.
Once you know the basics, you can also learn by solving Lean puzzles on Codewars.
Whatever resource you choose to use from the above list, it could be useful to have a copy of our tactic cheat sheet at hand, for reference.
If you prefer reading a book (with exercises), the standard reference is Theorem Proving in Lean. You almost certainly want to read it at some point anyway, since it explains foundational things much better than any hands-on tutorial could do.
If you are very new to the concept of logic and proofs, you can read Logic and Proof, a textbook that is a first rigorous proving course that teaches Lean at the same time.
If you have a computer science background, and are primarily interested in software verification, then you can read The Hitchhiker's Guide to Logical Verification (pdf), course notes for an MSc-level course at VU Amsterdam.
If you want a systematic exposition of syntax and commands, then you can read the reference manual.
In addition to the above sources, we have a number of small documents covering specific topics:
After using Lean for a while, you may want to learn how to write your own tactics. This is less documented than proof writing, but you can still have a look at the following resources.
If you are interested in foundations of Lean, you can first read a very rough sketch here. If you want a bit more detail, you can read the first chapter of the HoTT book, ignoring anything where univalence is mentioned.
Another potentially useful resource is this page from Coq's documentation. The foundations of Coq are very very close to those of Lean. The most relevant differences to keep in mind are:
Propis proof-irrelevant, so it is closer to
SPropfrom the page above.
If you can read the above Coq documentation then you are ready for this paper by Mario Carneiro which precisely describes the type theory of Lean.
Note that understanding type theoretic foundations is not at all necessary to use Lean.
A number of meetings have helped welcome newcomers to the Lean community. The following have links to online talks and other material that may be of interest: