Besides Lean's general documentation, the documentation of mathlib consists of:

• A guide on installing Lean and mathlib with elan.
• A description of currently covered theories, as well as an overview for mathematicians.
• A description of tactics introduced in mathlib, and available hole commands.
• An explanation of naming conventions that is useful to find or contribute definitions and lemmas.
• A style guide for contributors
• An outline of how to contribute to mathlib.
• A tentative list of work in progress to make sure efforts are not duplicated without collaboration.

This repository also contains extra Lean documentation not specific to mathlib.

Linux/OS X/Cygwin/MSYS2/git bash: run the following command in a terminal:

curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/scripts/remote-install-update-mathlib.sh -sSf | sh

Any platform: in the release section of this page, download mathlib-scripts-###-###-###.tar.gz, expand it and run setup-update-mathlib.sh.

In a terminal, in the directory of a project depending on mathlib, run the following:

update-mathlib

The existing _target/deps/mathlib will be rewritten with a compiled version of mathlib.

The following command, run on each project, sets up an automatic update of the mathlib binaries after every git checkout.

echo \#! /bin/sh > .git/hooks/post-checkout
echo update-mathlib >> .git/hooks/post-checkout
chmod +x .git/hooks/post-checkout

• Jeremy Avigad (@avigad): analysis
• Reid Barton (@rwbarton): category theory, topology
• Mario Carneiro (@digama0): all (lead maintainer)
• Simon Hudon (@cipher1024): all
• Chris Hughes (@ChrisHughes24): group_theory, ring_theory, field_theory
• Robert Y. Lewis (@robertylewis): all
• Patrick Massot (@patrickmassot): documentation