Learning Lean #

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.

Hands-on approaches #

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.

Textbooks #

Miscellaneous topics #

In addition to the above sources, we have a number of small documents covering specific topics:

Metaprogramming and tactic writing #

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.

More on foundations #

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:

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.

Meetings #

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: