This is a page that lists many useful links related to the Lean Theorem Prover

Up to date version of these links

Main links

• Zulip: the Lean chatroom. Requires you to create an account. Ask any and all questions in the new members stream.
• Mathlib: the main library of Lean. Probably required for any nontrivial Lean project.
• Lean 3 on Github: the official current (frozen) version of Lean.
• Lean 3 Community Edition: a fork of the frozen Lean 3 repository maintained by the mathlib team.
• Lean 4 on Github: the next version of Lean under development.
• Leanprover official website.

Try Lean

• Try Lean in your browser.
• Try Lean + mathlib in your browser.

Learn Lean

• Kevin Buzzard's natural number game is a online interactive tutorial to Lean.
• Theorem Proving in Lean: a textbook to learn Lean with interactive code snippets.
• Logic and Proof: a textbook that is a first rigorous proving course that teaches Lean at the same time.
• Logical Verification in Lean (pdf): course notes for a course at VU Amsterdam.
• Video tutorial of type theory and Lean.
• Lean tutorial: a file with many descriptive comments.
• Ask questions in the new members stream on Zulip.

Installation

You are strongly recommended to follow only the installation instructions provided in the mathlib repository. (The installation instructions on the downloads page are not recommended). Here are the links to the OSs:

• On Debian-derived Linux (Debian, Ubuntu, LMDE...)
• On other Linux
• On MacOS
• On Windows

Don't forget to also follow the instructions on Lean Projects.

• If you want to compile mathlib yourself (not recommended unless you only want to use very low-level files), you can skip the steps under Installing mathlib supporting tools. Compiling all of mathlib will probably take more than an hour.
• If you want to contribute to mathlib, here are some useful pointers.

Reference material

• Lean Reference Manual.
• Mathlib documentation
• Lean tactics for Coq users.
• Tactics in mathlib.

Community

• Zulip is a chat room where most of the action happens.
• leanprover-community website. This includes:
  • Zulip archive
  • Mathlib documentation
• There are also discussions on the mathlib issue tracker and pull requests.
• IMO Grand Challenge: a grand challenge to write an AI that can write formal proofs of IMO problems.

FAQs

• FAQ of the Lean 3 repository
• FAQ in this repository (currently empty)

How to Write Lean Tactics

• Tactics writing tutorial
• Programming in Lean: chapters 8 and 9 might be useful if you want to learn to write tactics.

Lean papers

• We provide a .bib file which collects Lean-related papers.
• Official list of publications

Papers about Lean

• Mario Carneiro. The Type Theory of Lean. Master thesis, 2019.
  • Meta-theoretic properties of Lean 3, including soundness.
• Sebastian Ullrich, Leonardo de Moura. Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming. preprint 2019.
  • Reference counting in Lean 4 (appendix, partial formalization, bachelor thesis about partial formalization).
• Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. A metaprogramming framework for formal verification. ICFP 2017.
  • Metaprogramming in Lean 3.
• Daniel Selsam and Leonardo de Moura. Congruence Closure in Intensional Type Theory. IJCAR 2016.
  • Congruence closure in Lean 3.
• Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer. The Lean Theorem Prover (System Description). CADE 2015.
  • System description of Lean 2
• Leonardo de Moura, Jeremy Avigad, Soonho Kong, Cody Roux. Elaboration in Dependent Type Theory. 2015 (unpublished).
  • Elaboration in Lean 2.

Papers using Lean

• The mathlib Community. The Lean mathematical library. CPP 2020.
  • mathlib
• Kevin Buzzard, Johan Commelin, Patrick Massot. Formalising perfectoid spaces. CPP 2020.
  • Formalization
• Jesse Michael Han and Floris van Doorn. A Formal Proof of the Independence of the Continuum Hypothesis.) CPP 2020.
  • Formalization / Website
• Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis. (Formalizing the Solution to the Cap Set Problem.) ITP 2019.
  • Formalization
• Minchao Wu and Rajeev Goré. Verified decision procedures for modal logics. ITP 2019.
  • Formalization
• Mario Carneiro. Formalizing computability theory via partial recursive functions. ITP 2019.
  • Formalization in mathlib/computability
• Jesse Michael Han and Floris van Doorn. A formalization of forcing and the unprovability of the continuum hypothesis. ITP 2019.
  • Formalization / Website
• Jeremy Avigad, Mario Carneiro, and Simon Hudon. Data types as quotients of polynomial functors. ITP 2019.
  • Formalization
• Juneyoung Lee, Chung-Kil Hur, and Nuno P. Lopes AliveInLean: A Verified LLVM Peephole Optimization Verifier.) CAV 2019.
  • Formalization / Website
• Robert Y. Lewis. A formal proof of Hensel's lemma over the p-adic integers. CPP 2019.
  • The formalization is part of mathlib. Website.
• Daniel Selsam, Percy Liang, David L. Dill Developing Bug-Free Machine Learning Systems With Formal Mathematics. ICML 2017.
  • Formalization
• Robert Y. Lewis. A bi-directional extensible ad hoc interface between Lean and Mathematica.) PxTP 2017.
  • Formalization / Website

Unpublished works using Lean

• Paul-Nicolas Madelaine. Arithmetic and Casting in Lean.. Master thesis, 2019.
  • A description of the norm_cast tactic in mathlib.
• Neil Strickland, Nicola Bellumat Iterated chromatic localisation.) arXiv 2019.
  • Formalization
• Marc Huisinga. Formally Verified Insertion of Reference Counting Instructions. Bachelor thesis, 2019.
  • Formalization
• Ramon Fernández Mir. (Schemes in Lean.) project report 2019.
  • Formalization
• More reports/theses are listed on the Lean Forward project page.

Main Repositories

• The core library ships with Lean.
• mathlib: main library of Lean.
• mathlib archive: some formalization projects maintained by mathlib maintainers.

Conferences

• Lean Together 2019 (recorded videos)
• Lean Together 2020

Lean 4

Lean 4 is the next version of Lean. It was made public early 2019, but is still missing certain core features as of October 2019 (such as a tactic framework)

• Lean 4 on Github: the source code.
• Lean 4: a guided preview: a presentation about Lean 4 at Lean Together 2019.
• Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming: reference counting in Lean 4.

HoTT in Lean

Homotopy type theory is not actively maintained in Lean. Here are some pointers to past projects:

• The Lean 2 HoTT library.
• The Spectral repository in Lean 2, doing more synthetic homotopy theory and formalizing the Serre spectral sequence.
• The Lean 3 HoTT library (much smaller, not officially supported by Lean).

Papers using Lean 2

• Constructing the Propositional Truncation using Non-recursive HITs (code).
• The Cayley-Dickson Construction in Homotopy Type Theory (code).
• The real projective spaces in homotopy type theory (code).
• Higher Groups in Homotopy Type Theory (code).