Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.
Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.
Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".
License: APACHE
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
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:
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
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