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.
Two options are avaiblable to install
- 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
Fetch mathlib binaries
In a terminal, in the directory of a project depending on mathlib, run the following:
_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
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