mathlib4
Mathlib is a user maintained library for the Lean theorem prover. It contains both programming infrastructure and mathematics, as well as tactics that use the former and allow to develop the latter.
Installation
You can find detailed instructions to install Lean, mathlib, and supporting tools on our website. Alternatively, click on the button below to open a Gitpod workspace containing the project.
Using mathlib4
as a dependency
Please refer to https://github.com/leanprovercommunity/mathlib4/wiki/Usingmathlib4asadependency
Experimenting
Got everything installed? Why not start with the tutorial project?
For more pointers, see Learning Lean.
Documentation
Besides the installation guides above and Lean's general documentation, the documentation of mathlib consists of:
 The mathlib4 docs: documentation generated
automatically from the source
.lean
files.  A description of currently covered theories, as well as an overview for mathematicians.
 Some extra Lean documentation not specific to mathlib (see "Miscellaneous topics")
 Documentation for people who would like to contribute to mathlib
Much of the discussion surrounding mathlib occurs in a Zulip chat room, and you are welcome to join, or read along without signing up. Questions from users at all levels of expertise are welcome! We also provide an archive of the public discussions, which is useful for quick reference.
Contributing
The complete documentation for contributing to mathlib
is located
on the community guide contribute to mathlib
The process is different from other projects where one should not fork the repository.
Instead write permission for nonmaster branches should be requested on Zulip
by introducing yourself, providing your GitHub handle and what contribution you are planning on doing.
You may want to subscribe to the mathlib4
stream

To obtain precompiled
olean
files, runlake exe cache get
. (Skipping this step means the next step will be very slow.) 
To build
mathlib4
runlake build
. 
To build and run all tests, run
lake test
. 
You can use
lake build Mathlib.Import.Path
to build a particular file, e.g.lake build Mathlib.Algebra.Group.Defs
. 
If you added a new file, run the following command to update
Mathlib.lean
lake exe mk_all
Guidelines
Mathlib has the following guidelines and conventions that must be followed
 The style guide
 A guide on the naming convention
 The documentation style
Downloading cached build files
You can run lake exe cache get
to download cached build files that are computed by mathlib4
's automated workflow.
If something goes mysteriously wrong,
you can try one of lake clean
or rm rf .lake
before trying lake exe cache get
again.
In some circumstances you might try lake exe cache get!
which redownloads cached build files even if they are available locally.
Call lake exe cache
to see its help menu.
Building HTML documentation
Building HTML documentation locally is straightforward, but it may take a while (>20 minutes):
lake R Kdoc=on update docgen4
lake build Mathlib:docs
The HTML files can then be found in build/doc
.
Warning: these commands will make a change to lakemanifest.json
which should not be committed to Mathlib.
Transitioning from Lean 3
For users familiar with Lean 3 who want to get up to speed in Lean 4 and migrate their existing Lean 3 code we have:
 A survival guide for Lean 3 users
 Instructions to run
mathport
on a project other than mathlib.mathport
is the tool the community used to port the entirety ofmathlib
from Lean 3 to Lean 4.
Dependencies
If you are a mathlib contributor and want to update dependencies, use lake update
,
or lake update batteries aesop
(or similar) to update a subset of the dependencies.
This will update the lakemanifest.json
file correctly.
You will need to make a PR after committing the changes to this file.
Please do not run lake update Kdoc=on
as previously advised, as the documentation related
dependencies should only be included when CI is building documentation.
Maintainers:
For a list containing more detailed information, see https://leanprovercommunity.github.io/teams/maintainers.html
 Anne Baanen (@Vierkantor): algebra, number theory, tactics
 Matthew Robert Ballard (@mattrobball): algebra, algebraic geometry, category theory, performance
 Reid Barton (@rwbarton): category theory, topology
 Riccardo Brasca (@riccardobrasca): algebra, number theory, algebraic geometry, category theory
 Kevin Buzzard (@kbuzzard): algebra, number theory, algebraic geometry, category theory
 Mario Carneiro (@digama0): lean formalization, tactics, type theory, proof engineering
 Bryan Ginge Chen (@bryangingechen): documentation, infrastructure
 Johan Commelin (@jcommelin): algebra, number theory, category theory, algebraic geometry
 Anatole Dedecker (@ADedecker): topology, functional analysis, calculus
 Rémy Degenne (@RemyDegenne): probability, measure theory, analysis
 Floris van Doorn (@fpvandoorn): measure theory, model theory, tactics
 Frédéric Dupuis (@dupuisf): linear algebra, functional analysis
 Gabriel Ebner (@gebner): tactics, infrastructure, core, formal languages
 Sébastien Gouëzel (@sgouezel): topology, calculus, geometry, analysis, measure theory
 Markus Himmel (@TwoFX): category theory
 Yury G. Kudryashov (@urkud): analysis, topology, measure theory
 Robert Y. Lewis (@robertylewis): tactics, documentation
 Jireh Loreaux (@jloreaux): analysis, topology, operator algebras
 Heather Macbeth (@hrmacbeth): geometry, analysis
 Patrick Massot (@patrickmassot): documentation, topology, geometry
 Bhavik Mehta (@bmehta): category theory, combinatorics
 Kyle Miller (@kmill): combinatorics, tactics, metaprogramming
 Kim Morrison (@semorrison): category theory, tactics
 Oliver Nash (@ocfnash): algebra, geometry, topology
 Joël Riou (@joelriou): category theory, homology, algebraic geometry
 Adam Topaz (@adamtopaz): algebra, category theory, algebraic geometry
 Eric Wieser (@ericwieser): algebra, infrastructure
Past maintainers:
 Jeremy Avigad (@avigad): analysis
 Johannes Hölzl (@johoelzl): measure theory, topology
 Simon Hudon (@cipher1024): tactics
 Chris Hughes (@ChrisHughes24): algebra