- 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.
- 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.
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:
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.
- Zulip is a chat room where most of the action happens.
- leanprover-community website. This includes:
- 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.
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.
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.
- 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.
- Kevin Buzzard, Johan Commelin, Patrick Massot. Formalising perfectoid spaces. CPP 2020.
- Jesse Michael Han and Floris van Doorn. A Formal Proof of the Independence of the Continuum Hypothesis. CPP 2020.
- Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis. Formalizing the Solution to the Cap Set Problem. ITP 2019.
- Minchao Wu and Rajeev Goré. Verified decision procedures for modal logics. ITP 2019.
- 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.
- Jeremy Avigad, Mario Carneiro, and Simon Hudon. Data types as quotients of polynomial functors. ITP 2019.
- Juneyoung Lee, Chung-Kil Hur, and Nuno P. Lopes AliveInLean: A Verified LLVM Peephole Optimization Verifier. CAV 2019.
- Robert Y. Lewis. A formal proof of Hensel's lemma over the p-adic integers. CPP 2019.
- Daniel Selsam, Percy Liang, David L. Dill Developing Bug-Free Machine Learning Systems With Formal Mathematics. ICML 2017.
- Robert Y. Lewis. A bi-directional extensible ad hoc interface between Lean and Mathematica. PxTP 2017.
Unpublished works using Lean
- Paul-Nicolas Madelaine. Arithmetic and Casting in Lean.. Internship report, 2019.
- A description of the
norm_casttactic in mathlib.
- A description of the
- Neil Strickland, Nicola Bellumat Iterated chromatic localisation. arXiv 2019.
- Marc Huisinga. Formally Verified Insertion of Reference Counting Instructions. Bachelor thesis, 2019.
- Ramon Fernández Mir. Schemes in Lean. Project report, 2019.
- More reports/theses are listed on the Lean Forward project page.
- The core library ships with Lean.
- mathlib: main library of Lean.
- mathlib archive: some formalization projects maintained by mathlib maintainers.
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).
- We provide a .bib file which collects Lean-related papers.