leanprover-community / links

This is a page that lists many useful links related to the Lean Theorem Prover. Please submit additions and updates via GitHub.

Try Lean

Learn Lean


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.

Reference material



How to Write Lean Tactics

Lean papers

Papers about Lean

Papers using Lean

Unpublished works using Lean

Main Repositories


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)

HoTT in Lean

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

Papers using Lean 2


  • We provide a .bib file which collects Lean-related papers.