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 one of the buttons below to open a GitHub Codespace or a Gitpod workspace containing the project.

Using `mathlib4` as a dependency

Please refer to
https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

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

You may want to subscribe to the mathlib4 channel on Zulip to introduce yourself and your plan to the community.
Often you can find community members willing to help you get started and advise you on the fit and
feasibility of your project.

To obtain precompiled olean files, run lake exe cache get. (Skipping this step means the next step will be very slow.)
To build mathlib4 run lake 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
```
shell
lake exe mk_all
```

Guidelines

Mathlib has the following guidelines and conventions that must be followed

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 re-downloads cached build files even if they are available locally.

Call lake exe cache to see its help menu.

Building HTML documentation

The mathlib4_docs repository
is responsible for generating and publishing the
mathlib4 docs.

That repo can be used to build the docs locally:

shell
git clone https://github.com/leanprover-community/mathlib4_docs.git
cd mathlib4_docs
cp ../mathlib4/lean-toolchain .
lake exe cache get
lake build Mathlib:docs

The last step may take a while (>20 minutes).
The HTML files can then be found in .lake/build/doc.

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
of mathlib 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 lake-manifest.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://leanprover-community.github.io/teams/maintainers.html

Anne Baanen (@Vierkantor): algebra, number theory, tactics
Matthew Robert Ballard (@mattrobball): algebra, algebraic geometry, category theory
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 Gin-ge 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
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 (@j-loreaux): analysis, topology, operator algebras
Heather Macbeth (@hrmacbeth): geometry, analysis
Patrick Massot (@patrickmassot): documentation, topology, geometry
Bhavik Mehta (@b-mehta): category theory, combinatorics
Kyle Miller (@kmill): combinatorics, tactics, metaprogramming
Kim Morrison (@kim-em): category theory, tactics
Oliver Nash (@ocfnash): algebra, geometry, topology
Filippo A. E. Nuccio (@faenuccio): algebra, functional analysis, homology, number theory
Joël Riou (@joelriou): category theory, homology, algebraic geometry
Michael Rothgang (@grunweg): differential geometry, analysis, topology, linters
Damiano Testa (@adomani): algebra, algebraic geometry, number theory, tactics, linters
Adam Topaz (@adamtopaz): algebra, category theory, algebraic geometry
Eric Wieser (@eric-wieser): algebra, infrastructure