This webpage is about Lean 3, which is effectively obsolete; the community has migrated to Lean 4.

Jump to the corresponding page on the main Lean 4 website.

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 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.
The lfctm2020 exercises, developed for the July 2020 virtual meeting Lean for the Curious Mathematician, are another good resource. There are corresponding tutorial videos from the meeting.
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 project.
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.

Textbooks #

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) (tablet edition optimized for on-screen viewing), 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.

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.

The tactic writing tutorial covers the basics and enables you to read more advanced sources, for instance the code of existing tactics.
The Hitchhiker's Guide to Logical Verification (pdf) also has a chapter on metaprogramming.
The reference paper on Lean metaprogramming.
The metaprogramming tutorial videos that Rob Lewis designed and recorded for LftCM 2020.

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:

Lean's Prop is proof-irrelevant, so it is closer to SProp from the page above.
Universes in Lean are not cumulative. However, any type can be lifted to higher universes.
Lean natively supports quotient types and their associated reduction rule (see this section of Theorem proving in Lean).

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:

We also have a YouTube channel which includes playlists of videos from the above conferences, and also other conferences with Lean-relevant content.

Miscellaneous resources #

lean-for-hackers: a hands-on guide to using Lean 3 as a programming language.