base on The math library of Lean 4 # mathlib4  [](https://mathlib-bors-ca18eefec4cb.herokuapp.com/repositories/16) [](https://leanprover.zulipchat.com) [](https://gitpod.io/#https://github.com/leanprover-community/mathlib4) [Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean theorem prover](https://leanprover.github.io). 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, mathlib, and supporting tools on [our website](https://leanprover-community.github.io/get_started.html). Alternatively, click on one of the buttons below to open a GitHub Codespace or a Gitpod workspace containing the project. [](https://codespaces.new/leanprover-community/mathlib4) [](https://gitpod.io/#https://github.com/leanprover-community/mathlib4) ## 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 Got everything installed? Why not start with the [tutorial project](https://leanprover-community.github.io/install/project.html)? For more pointers, see [Learning Lean](https://leanprover-community.github.io/learn.html). ## Documentation Besides the installation guides above and [Lean's general documentation](https://docs.lean-lang.org/lean4/doc/), the documentation of mathlib consists of: - [The mathlib4 docs](https://leanprover-community.github.io/mathlib4_docs/index.html): documentation [generated automatically](https://github.com/leanprover/doc-gen4) from the source `.lean` files. - A description of [currently covered theories](https://leanprover-community.github.io/theories.html), as well as an [overview](https://leanprover-community.github.io/mathlib-overview.html) for mathematicians. - Some [extra Lean documentation](https://leanprover-community.github.io/learn.html) not specific to mathlib (see "Miscellaneous topics") - Documentation for people who would like to [contribute to mathlib](https://leanprover-community.github.io/contribute/index.html) 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. ## Contributing The complete documentation for contributing to ``mathlib`` is located [on the community guide contribute to mathlib](https://leanprover-community.github.io/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. You may want to subscribe to the `mathlib4` stream * To obtain precompiled `olean` files, run `lake exe cache get`. (Skipping this step means the next step will be very slow.) * To build `mathlib4` run `lake build`. * To build and run all tests, run `lake test`. * You can use `lake build Mathlib.Import.Path` to build a particular file, e.g. `lake build Mathlib.Algebra.Group.Defs`. * If you added a new file, run the following command to update `Mathlib.lean` ```shell lake exe mk_all ``` ### Guidelines Mathlib has the following guidelines and conventions that must be followed - The [style guide](https://leanprover-community.github.io/contribute/style.html) - A guide on the [naming convention](https://leanprover-community.github.io/contribute/naming.html) - The [documentation style](https://leanprover-community.github.io/contribute/doc.html) ### 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 The [mathlib4_docs repository](https://github.com/leanprover-community/mathlib4_docs) is responsible for generating and publishing the [mathlib4 docs](https://leanprover-community.github.io/mathlib4_docs/index.html). That repo can be used to build the docs locally: ```shell git clone https://github.com/leanprover-community/mathlib4_docs.git cd mathlib4_docs cp ../mathlib4/lean-toolchain . lake exe cache get lake build Mathlib:docs ``` 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: - A [survival guide](https://github.com/leanprover-community/mathlib4/wiki/Lean-4-survival-guide-for-Lean-3-users) for Lean 3 users - [Instructions to run `mathport`](https://github.com/leanprover-community/mathport#running-on-a-project-other-than-mathlib) on a project other than mathlib. `mathport` is the tool the community used to port the entirety of `mathlib` from Lean 3 to Lean 4. ### 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: For a list containing more detailed information, see https://leanprover-community.github.io/teams/maintainers.html * Anne Baanen (@Vierkantor): algebra, number theory, tactics * Matthew Robert Ballard (@mattrobball): algebra, algebraic geometry, category theory, performance * Reid Barton (@rwbarton): category theory, topology * 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 * Gabriel Ebner (@gebner): tactics, infrastructure, core, formal languages * 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 * Joël Riou (@joelriou): category theory, homology, algebraic geometry * Damiano Testa (@adomani): algebra, algebraic geometry, number theory, tactics * Adam Topaz (@adamtopaz): algebra, category theory, algebraic geometry * Eric Wieser (@eric-wieser): algebra, infrastructure ## Past maintainers: * Jeremy Avigad (@avigad): analysis * Johannes Hölzl (@johoelzl): measure theory, topology * Simon Hudon (@cipher1024): tactics * Chris Hughes (@ChrisHughes24): algebra ", Assign "at most 3 tags" to the expected json: {"id":"10581","tags":[]} "only from the tags list I provide: [{"id":77,"name":"3d"},{"id":89,"name":"agent"},{"id":17,"name":"ai"},{"id":54,"name":"algorithm"},{"id":24,"name":"api"},{"id":44,"name":"authentication"},{"id":3,"name":"aws"},{"id":27,"name":"backend"},{"id":60,"name":"benchmark"},{"id":72,"name":"best-practices"},{"id":39,"name":"bitcoin"},{"id":37,"name":"blockchain"},{"id":1,"name":"blog"},{"id":45,"name":"bundler"},{"id":58,"name":"cache"},{"id":21,"name":"chat"},{"id":49,"name":"cicd"},{"id":4,"name":"cli"},{"id":64,"name":"cloud-native"},{"id":48,"name":"cms"},{"id":61,"name":"compiler"},{"id":68,"name":"containerization"},{"id":92,"name":"crm"},{"id":34,"name":"data"},{"id":47,"name":"database"},{"id":8,"name":"declarative-gui "},{"id":9,"name":"deploy-tool"},{"id":53,"name":"desktop-app"},{"id":6,"name":"dev-exp-lib"},{"id":59,"name":"dev-tool"},{"id":13,"name":"ecommerce"},{"id":26,"name":"editor"},{"id":66,"name":"emulator"},{"id":62,"name":"filesystem"},{"id":80,"name":"finance"},{"id":15,"name":"firmware"},{"id":73,"name":"for-fun"},{"id":2,"name":"framework"},{"id":11,"name":"frontend"},{"id":22,"name":"game"},{"id":81,"name":"game-engine "},{"id":23,"name":"graphql"},{"id":84,"name":"gui"},{"id":91,"name":"http"},{"id":5,"name":"http-client"},{"id":51,"name":"iac"},{"id":30,"name":"ide"},{"id":78,"name":"iot"},{"id":40,"name":"json"},{"id":83,"name":"julian"},{"id":38,"name":"k8s"},{"id":31,"name":"language"},{"id":10,"name":"learning-resource"},{"id":33,"name":"lib"},{"id":41,"name":"linter"},{"id":28,"name":"lms"},{"id":16,"name":"logging"},{"id":76,"name":"low-code"},{"id":90,"name":"message-queue"},{"id":42,"name":"mobile-app"},{"id":18,"name":"monitoring"},{"id":36,"name":"networking"},{"id":7,"name":"node-version"},{"id":55,"name":"nosql"},{"id":57,"name":"observability"},{"id":46,"name":"orm"},{"id":52,"name":"os"},{"id":14,"name":"parser"},{"id":74,"name":"react"},{"id":82,"name":"real-time"},{"id":56,"name":"robot"},{"id":65,"name":"runtime"},{"id":32,"name":"sdk"},{"id":71,"name":"search"},{"id":63,"name":"secrets"},{"id":25,"name":"security"},{"id":85,"name":"server"},{"id":86,"name":"serverless"},{"id":70,"name":"storage"},{"id":75,"name":"system-design"},{"id":79,"name":"terminal"},{"id":29,"name":"testing"},{"id":12,"name":"ui"},{"id":50,"name":"ux"},{"id":88,"name":"video"},{"id":20,"name":"web-app"},{"id":35,"name":"web-server"},{"id":43,"name":"webassembly"},{"id":69,"name":"workflow"},{"id":87,"name":"yaml"}]" returns me the "expected json"