Learning Lean 4 #

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.

All the resources listed on this page are about Lean 4. Some have Lean 3 versions, but there is no point learning Lean 3 at this stage.

Hands-on approaches #

Whatever your background, if you want to dive right away, you can play the Natural Number Game. This is an online interactive Lean tutorial focused on proving properties of the elementary operations on natural numbers. The Lean Game Server hosts various learning games including Set Theory, Logic, and Robo (a story about undergrad mathematics).
For a faster-paced dive, you can get the Glimpse of Lean tutorial. This contains four basic files covering some fundamental aspects of proving using Lean, and then independent topic files about elementary analysis, abstract topology and mathematical logic.

Books #

If you prefer reading a book (with exercises), there are a number of freely available Lean books. These are available as html or PDFs, but are usually meant to be read interactively in VSCode, doing Lean exercises on the fly:

The standard mathematics-oriented reference is Mathematics in Lean. You can download it as a pdf, but see also the VSCode instructions).
The Mechanics of Proof is also mathematics-oriented. It has a gentler pace than Mathematics in Lean and is aimed at readers with less mathematical experience.
Formalising Mathematics: course notes for mathematicians, with useful tips and an overview of common tactics.
If you prefer something more about the foundations of type theory, the standard reference is Theorem Proving in Lean.
A computer-science/programming-oriented book is The Hitchhiker's Guide to Logical Verification. It also has useful information about the type theory of Lean, and an associated VSCode project with exercises.
If you want something more focused on Lean itself than on using Lean, then you can read the reference manual.

(Meta)-programming and tactic writing #

If you are interested in Lean as a programming language then you should read Functional programming in Lean.
If you specifically want to do meta-programming and write tactics then you can read Metaprogramming in Lean 4 (after at least checking you are comfortable with the monad chapters of Functional programming in Lean).

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.

If you're interested in the nuts and bolts of Lean's kernel, writing your own external type checker for Lean, or exporting proofs, you can read more in Type Checking in Lean 4.

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. Note that all items until the year 2022 used Lean 3, but they may still contain relevant information.

More events can be found on the events page. We also have a YouTube channel which includes playlists of videos from the above conferences, and also other conferences with Lean-relevant content.