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:
.leanfiles. In addition to the pages generated for each file in the library, the docs also include pages on:
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.
The complete documentation for contributing to
mathlib is located
on the community guide contribute to mathlib
The process is different from other projects where one should not fork the repository. Instead write permission for non-master branches should be requested on Zulip by introducing yourself, providing your GitHub handle and what contribution you are planning on doing.
Mathlib has the following guidelines and conventions that must be followed
Note: the title of a PR should follow the commit naming convention.
leanproject get -b mathlib:shiny_lemma command will create a new worktree
with a local branch called
shiny_lemma which has a copy of mathlib to work on.
leanproject build will check that nothing broke.
Be warned that this will take some time if a fundamental file was changed.