This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 298
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
2 changed files
with
116 additions
and
109 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,115 @@ | ||
| # Lean 3's mathlib | ||
|
|
||
| > [!WARNING] | ||
| > Lean 3 and Mathlib 3 are no longer actively maintained. | ||
| > It is strongly recommended that you use [mathlib4](https://github.com/leanprover-community/mathlib4) for Lean 4 instead. | ||
|  | ||
| [](https://app.bors.tech/repositories/24316) | ||
| [](https://leanprover.zulipchat.com) | ||
| [](https://gitpod.io/#https://github.com/leanprover-community/mathlib) | ||
|
|
||
| [Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean 3 theorem prover](https://github.com/leanprover-community/lean). | ||
| It contains both programming infrastructure and mathematics, | ||
| as well as tactics that use the former and allow to develop the latter. | ||
|
|
||
| ## Installation | ||
|
|
||
| You can find detailed instructions to install Lean 3, mathlib 3, and supporting tools on [our website](https://leanprover-community.github.io/lean3/get_started.html). | ||
|
|
||
| ## Experimenting | ||
|
|
||
| Got everything installed? Why not start with the [tutorial project](https://leanprover-community.github.io/lean3/install/project.html)? | ||
|
|
||
| For more pointers, see [Learning Lean](https://leanprover-community.github.io/lean3/learn.html). | ||
|
|
||
| ## Documentation | ||
|
|
||
| Besides the installation guides above and [Lean's general | ||
| documentation](https://leanprover.github.io/lean3/documentation/), the documentation | ||
| of mathlib consists of: | ||
|
|
||
| - [The mathlib docs](https://leanprover-community.github.io/mathlib_docs): documentation [generated | ||
| automatically](https://github.com/leanprover-community/doc-gen) from the source `.lean` files. | ||
| In addition to the pages generated for each file in the library, the docs also include pages on: | ||
| - [tactics](https://leanprover-community.github.io/mathlib_docs/tactics.html), | ||
| - [commands](https://leanprover-community.github.io/mathlib_docs/commands.html), | ||
| - [hole commands](https://leanprover-community.github.io/mathlib_docs/hole_commands.html), and | ||
| - [attributes](https://leanprover-community.github.io/mathlib_docs/attributes.html). | ||
| - A description of [currently covered theories](https://leanprover-community.github.io/theories.html), | ||
| as well as an [overview](https://leanprover-community.github.io/lean3/mathlib-overview.html) for mathematicians. | ||
| - A couple of [tutorial Lean files](docs/tutorial/) | ||
| - Some [extra Lean documentation](https://leanprover-community.github.io/lean3/learn.html) not specific to mathlib (see "Miscellaneous topics") | ||
| - Documentation for people who would like to [contribute to mathlib3](https://leanprover-community.github.io/lean3/contribute/index.html) | ||
|
|
||
| Much of the discussion surrounding mathlib occurs in a | ||
| [Zulip chat room](https://leanprover.zulipchat.com/). Since this | ||
| chatroom is only visible to registered users, we provide an | ||
| [openly accessible archive](https://leanprover-community.github.io/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. | ||
|
|
||
| ## Contributing | ||
|
|
||
| > [!WARNING] | ||
| > Contributions are no longer accepted to mathlib 3; contribute to mathlib 4 instead! | ||
| The complete documentation for contributing to ``mathlib`` is located | ||
| [on the community guide contribute to mathlib](https://leanprover-community.github.io/lean3/contribute/index.html) | ||
|
|
||
| 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](https://leanprover.zulipchat.com) | ||
| by introducing yourself, providing your GitHub handle and what contribution you are planning on doing. | ||
|
|
||
| ### Guidelines | ||
|
|
||
| Mathlib has the following guidelines and conventions that must be followed | ||
|
|
||
| - The [style guide](https://leanprover-community.github.io/lean3/contribute/style.html) | ||
| - A guide on the [naming convention](https://leanprover-community.github.io/lean3/contribute/naming.html) | ||
| - The [documentation style](https://leanprover-community.github.io/lean3/contribute/doc.html) | ||
| - The [commit naming conventions](https://github.com/leanprover-community/lean/blob/master/doc/commit_convention.md) | ||
|
|
||
| Note: the title of a PR should follow the commit naming convention. | ||
|
|
||
| ### Using ``leanproject`` to contribute | ||
|
|
||
| Running the ``leanproject get -b mathlib:shiny_lemma`` command will create a new worktree ``mathlib_shiny_lemma`` | ||
| 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. | ||
|
|
||
| ## Maintainers: | ||
|
|
||
| * Anne Baanen (@Vierkantor): algebra, number theory, tactics | ||
| * Reid Barton (@rwbarton): category theory, topology | ||
| * Riccardo Brasca (@riccardobrasca): algebra, number theory, algebraic geometry, category theory | ||
| * 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 | ||
| * Frédéric Dupuis (@dupuisf): linear algebra, functional analysis | ||
| * 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 | ||
| * Kyle Miller (@kmill): combinatorics, documentation | ||
| * 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 | ||
|
|
||
| ## Emeritus maintainers: | ||
|
|
||
| * Jeremy Avigad (@avigad): analysis | ||
| * Johannes Hölzl (@johoelzl): measure theory, topology | ||
| * Simon Hudon (@cipher1024): tactics |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters