Lean mathlib

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 later.

Installation

You can find detailed instructions to install Lean, mathlib, and supporting tools:

• On Debian-derived Linux (Debian, Ubuntu, LMDE...)
• On other Linux distributions
• On MacOS
• On Windows

Documentation

Besides the installation guides above and Lean's general
documentation, the documentation
of mathlib consists of:

• A description of currently covered theories,
  as well as an overview for mathematicians.
• A couple of tutorials
• Some extra Lean documentation not specific to mathlib
• A description of tactics introduced in mathlib,
  and available hole commands.
• Documentation for people who would like to contribute to mathlib

Much of the discussion surrounding mathlib occurs in a
Zulip chat room. Since this
chatroom is only visible to registered users, we provide an
openly accessible archive
of the public discussions. This is useful for quick reference; for a
better browsing interface, and to participate in the discussions, we strongly
suggest joining the chat. Questions from users at all levels of expertise are
welcomed.

Maintainers:

• Jeremy Avigad (@avigad): analysis
• Reid Barton (@rwbarton): category theory, topology
• Mario Carneiro (@digama0): all (lead maintainer)
• Johan Commelin (@jcommelin): algebra
• Floris van Doorn (@fpvandoorn): all
• Sébastien Gouëzel (@sgouezel): topology, calculus
• Simon Hudon (@cipher1024): all
• Chris Hughes (@ChrisHughes24): group theory, ring theory, field theory
• Robert Y. Lewis (@robertylewis): all
• Scott Morrison (@semorrison): category theory