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.
You can find detailed instructions to install Lean, mathlib, and supporting tools on our website.
Got everything installed? Why not start with the tutorial project?
For more pointers, see Learning Lean.
Besides the installation guides above and Lean's general documentation, the documentation of mathlib consists of:
- The mathlib docs: documentation generated
automatically from the source
.leanfiles. In addition to the pages generated for each file in the library, the docs also include pages on:- tactics,
- commands,
- hole commands, and
- attributes.
- A description of currently covered theories, as well as an overview for mathematicians.
- A couple of tutorial Lean files
- 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. 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.
- Anne Baanen (@Vierkantor): algebra, number theory, tactics
- Reid Barton (@rwbarton): category theory, topology
- 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
- Rémy Degenne (@RemyDegenne): probability, measure theory, analysis
- Floris van Doorn (@fpvandoorn): measure theory, model theory, tactics
- Gabriel Ebner (@gebner): tactics, infrastructure, core, formal languages
- Sébastien Gouëzel (@sgouezel): topology, calculus, geometry, analysis, measure theory
- Markus Himmel (@TwoFX): category theory
- Chris Hughes (@ChrisHughes24): algebra
- Yury G. Kudryashov (@urkud): analysis, topology, measure theory
- Robert Y. Lewis (@robertylewis): tactics, documentation
- Heather Macbeth (@hrmacbeth): geometry, analysis
- Patrick Massot (@patrickmassot): documentation, topology, geometry
- Bhavik Mehta (@b-mehta): category theory, combinatorics
- Scott Morrison (@semorrison): category theory, tactics
- Oliver Nash (@ocfnash): algebra, geometry, topology
- Adam Topaz (@adamtopaz): algebra, category theory, algebraic geometry
- Eric Wieser (@eric-wieser): algebra, infrastructure
- Jeremy Avigad (@avigad): analysis
- Johannes Hölzl (@johoelzl): measure theory, topology
- Simon Hudon (@cipher1024): tactics