Learning Lean #

There are ways to start learning Lean, depending on your background and taste. There 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 #

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.