leanprover-community/mathlib4

# mathlib4 ## Installation ## Using `mathlib4` as a dependency Please refer to [https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency](https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency) ## Experimenting ## Documentation Besides the installation guides above and [Lean's general documentation](https://docs.lean-lang.org/lean4/doc/), the documentation of mathlib consists of: Much of the discussion surrounding mathlib occurs in a [Zulip chat room](https://leanprover.zulipchat.com/), and you are welcome to join, or read along without signing up. Questions from users at all levels of expertise are welcome! We also provide an [archive of the public discussions](https://leanprover-community.github.io/archive/), which is useful for quick reference. ### Guidelines Mathlib has the following guidelines and conventions that must be followed ### Downloading cached build files You can run `lake exe cache get` to download cached build files that are computed by `mathlib4`'s automated workflow. If something goes mysteriously wrong, you can try one of `lake clean` or `rm -rf .lake` before trying `lake exe cache get` again. In some circumstances you might try `lake exe cache get!` which re-downloads cached build files even if they are available locally. Call `lake exe cache` to see its help menu. ### Building HTML documentation That repo can be used to build the docs locally: The last step may take a while (>20 minutes). The HTML files can then be found in `.lake/build/doc`. ## Transitioning from Lean 3 For users familiar with Lean 3 who want to get up to speed in Lean 4 and migrate their existing Lean 3 code we have: ### Dependencies If you are a mathlib contributor and want to update dependencies, use `lake update`, or `lake update batteries aesop` (or similar) to update a subset of the dependencies. This will update the `lake-manifest.json` file correctly. You will need to make a PR after committing the changes to this file. Please do not run `lake update -Kdoc=on` as previously advised, as the documentation related dependencies should only be included when CI is building documentation. ## Maintainers: * Anne Baanen (@Vierkantor): algebra, number theory, tactics * Matthew Robert Ballard (@mattrobball): algebra, algebraic geometry, category theory * Riccardo Brasca (@riccardobrasca): algebra, number theory, algebraic geometry, category theory * Kevin Buzzard (@kbuzzard): 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 * Anatole Dedecker (@ADedecker): topology, functional analysis, calculus * 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 * Sébastien Gouëzel (@sgouezel): topology, calculus, geometry, analysis, measure theory * Markus Himmel (@TwoFX): category theory * Yury G. Kudryashov (@urkud): analysis, topology, measure theory * Robert Y. Lewis (@robertylewis): tactics, documentation * Jireh Loreaux (@j-loreaux): analysis, topology, operator algebras * Heather Macbeth (@hrmacbeth): geometry, analysis * Patrick Massot (@patrickmassot): documentation, topology, geometry * Bhavik Mehta (@b-mehta): category theory, combinatorics * Kyle Miller (@kmill): combinatorics, tactics, metaprogramming * Kim Morrison (@kim-em): category theory, tactics * Oliver Nash (@ocfnash): algebra, geometry, topology * Filippo A. E. Nuccio (@faenuccio): algebra, functional analysis, homology, number theory * Joël Riou (@joelriou): category theory, homology, algebraic geometry * Michael Rothgang (@grunweg): differential geometry, analysis, topology, linters * Damiano Testa (@adomani): algebra, algebraic geometry, number theory, tactics, linters * Adam Topaz (@adamtopaz): algebra, category theory, algebraic geometry * Eric Wieser (@eric-wieser): algebra, infrastructure ## Past maintainers: * Jeremy Avigad (@avigad): analysis * Reid Barton (@rwbarton): category theory, topology * Gabriel Ebner (@gebner): tactics, infrastructure, core, formal languages * Johannes Hölzl (@johoelzl): measure theory, topology * Simon Hudon (@cipher1024): tactics * Chris Hughes (@ChrisHughes24): algebra