Lean Theorem Prover Mathlib

Summary

mathlib4 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 latter. Installation You can find detailed instructions to install Lean, mathlib, and supporting tools on our website. Alternatively, click on one of the buttons below to open a GitHub Codespace or a Gitpod workspace containing the project. Using mathlib4 as a dependency Please refer to https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency Experimenting Got everything installed? Why not start with the tutorial project? For more pointers, see Learning Lean. Documentation Besides the installation guides above and Lean's general documentation, the documentation of mathlib consists of: Much of the discussion surrounding mathlib occurs in a Zulip chat room, 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, which is useful for quick reference. Contributing The complete documentation for contributing to mathlib is located on the community guide contribute to mathlib You may want to subscribe to the mathlib4 channel on Zulip to introduce yourself and your plan to the community. Often you can find community members willing to help you get started and advise you on the fit and feasibility of your project. 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 lake exe mk_all Guidelines Mathlib has the following guidelines and conventions that must be followed Downloading cached build files You ca...