Skip to content

leanprover-community-bot/mathlib

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Lean mathlib

Mergify Status

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:

Experimenting

Got everything installed? Why not start with the tutorial project?

For more pointers, see Lean Links.

Documentation

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

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
  • Gabriel Ebner (@gebner): 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
  • Patrick Massot (@patrickmassot): documentation, topology
  • Scott Morrison (@semorrison): category theory
  • Yury G. Kudryashov (@urkud): analysis, topology

Packages

No packages published

Languages

  • Lean 99.9%
  • Other 0.1%