Resources

Summary

Start by playing the natural number game in your browser. Then follow the instructions to download Lean on your computer and start working through the tutorials project (aka Patrick Massot's tutorial). Along the way, make a Zulip account to ask questions on the Lean Zulip chat and read parts of Theorem Proving in Lean to better understand the basic rules and syntax of Lean. After that, work on other tutorials, try formalizing things on your own, and continue asking questions on the Zulip chat.

Tutorials

Recommendations: Start with the natural number game. Once you finish that, install Lean on your computer and then try out Patrick Massot's tutorial (also referred to as "the tutorials project" on the Lean community website). After that, try out some of the other tutorials, like Mathematics in Lean or the complex number game. Also try making an account on codewars and doing some of the exercises there. Along the way, fill in your knowledge of the basic rules of Lean by reading "Theorem Proving in Lean" (see "Background/References" section). At some point, start challenging yourself to formalize little things outside the framework of a tutorial or exercise.

  • The natural number game and solutions. A fairly friendly online game-style introduction to a subset of Lean

  • Patrick Massot's tutorial (aka "the tutorials project"). A series of exercises from an undergrad real analysis course, culminating in a proof of the intermediate value theorem. Explains more of the stuff you can do in Lean than the natural number game does. Requires you to install Lean on your computer (i.e. you can't complete it in your web browser).

  • Mathematics in Lean. A more comprehensive introduction to Lean, more in the style of a textbook. Still under development.

  • Complex number game. Shows how to define the complex numbers and prove their basic properties. Less polished than some of the other tutorials and still under development.

  • Lean on codewars and some instructions. The codewars website has a set of crowd-sourced exercises in Lean, varying in difficulty.

  • Math challenges for the Lean curious. A small collection of random exercises in Lean.

  • Exercises from "Lean for the Curious Mathematician." A collection of exercises from a recent workshop meant to introduce new Lean users to different parts of mathlib. These look like they could be very helpful.

  • Videos from "Lean for the Curious Mathematician." A collection of videos from a recent workshop. Covers the basics of Lean and an introduction to different parts of mathlib as well as other topics like writing tactics in Lean, installing Lean, using git & github, and the way Lean handles classes and structures.

How to use/install Lean

It is possible to use Lean in your browser without downloading anything to your computer. However, it is much slower in the browser and it is a good idea to install it on your computer at some point. Fortunately, the Lean community has prepared a guide for how to do this (although a few Windows users have encountered problems following it). If anything goes wrong, try asking for help on the Lean Zulip chat or during the seminar/problem sessions.

Background/References for Lean's dependent type theory

Recommendations: Lean formalizes math in a system called "dependent type theory." At some point it may become hard to formalize things in Lean without understanding something of this formal system. The textbook "Theorem Proving in Lean" provides a friendly (though somewhat dry) introduction to dependent type theory as well as a fairly systematic introduction to the syntax of Lean. It is probably a good idea to read at least some parts of that textbook to better understand the basic rules and syntax of Lean. The textbook "Logic and Proof" is somewhat similar, except that it is aimed at someone who is learning how to write mathematical proofs for the first time. Also included in the list below are some links that may help you better understand dependent type theory in general (outside the context of Lean).

  • Theorem Proving in Lean. A fairly comprehensive and systematic introduction to dependent type theory and the basic syntax of Lean. Very helpful to read if you are getting confused or frustrated by the underlying rules that Lean uses.

  • Logic and proof. Similar to "Theorem Proving in Lean" but slower paced, less comprehensive, and also contains an introduction to various basic math topics. It was written as a textbook for an "introduction to proofs" class taught using Lean, but it may be useful to look at to see how to develop basic math in Lean.

  • Reference Manual. This is intended to be a reference manual for Lean. However, it is still somewhat incomplete.

  • Intuitionistic type theory. A short book by Per Martin-Löf that lays out the basic rules of and motivation for dependent type theory.

  • BHK interpretation. Wikipedia article on the BHK interpretation, which was a major influence on the way propositions are treated in dependent type theory.

  • Curry-Howard correspondence. Expository article on the idea (sometimes called "propositions-as-types") that led to the development of dependent type theory.

Lean community

Lean has a very friendly and helpful community. The Zulip chat is very active and very often someone will answer your question within 5 minutes of when you ask it. Our seminar also has its own stream on the Zulip chat. Also the Lean community has set up a website with a lot of helpful information and links.

Mathlib reference

  • Documentation. A list of all the tactics, definitions, theorems, etc in mathlib.

  • List of tactics. A list of all the tactics in Lean/mathlib with some explanation on each one and, in some cases, helpful examples. This is part of the mathlib documentation linked to above.

  • Explanation of the leanproject command. You can also get much of this information by running "leanproject -h" in your terminal.

  • Repository. The source code for mathlib.

  • Contributing. Instructions about how to contribute to mathlib.

  • Projects. Some ideas for projects that could contribute to mathlib.

Contributing to mathlib

Miscellaneous

  • Sphere eversion project. An attempt to formalize the proof of sphere eversion in Lean. The proof has been divided into modular components so that people can contribute easily without having to understand the entire formalization attempt. May require substantial understanding of topology to contribute.

  • Consistency proof of Lean's type theory. Mario Carneiro's MS thesis which contains a proof that Lean's type theory is consistent relative to ZFC + the existence of countably many inaccessible cardinals. It contains a complete formal specification of the underlying logical rules of Lean, which does not seem to be available anywhere else online. If you have a logical or foundational question about Lean, this might be a good place to look. However, it is not a good way to learn how to use Lean (nor is it meant to be).

  • Progress on completing Freek's list in Lean. Freek Wiedijk maintains a list of 100 mathematical theorems (though he did not originate the list) and tracks which proof assistants they have been formalized in. Around 70 have been formalized in Lean so far (compared to 97 which have been formalized in any proof assistant).