mathlib

Lean standard library

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.

Obtaining binaries

Install the update-mathlib script

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-dev-scripts.sh.

Fetch mathlib binaries

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.

Automatic update of the binaries

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

Maintainers (topics):

• 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