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
... continue reading