repository·master·Indexed 25 days ago
https://github.com/leanprover-community/mathlib4A large-scale, community-maintained library for the Lean 4 theorem prover providing extensive mathematical infrastructure, theorems, and tactics. Includes documentation on the algebraic hierarchy, convex analysis, the Archive directory for niche formalizations (including IMO problems and Wiedijk's 100 Theorems), and the mathlib cache tool for managing pre-built .olean files.
The Mathlib/Probability/Combinatorics directory contains results related to probabilistic combinatorics, specifically focusing on the study of sampling combinatorial objects randomly.
Currently, the library provides definitions for:
The Mathlib/Geometry/Group/Growth subfolder contains mathematical results concerning the growth of finitely generated groups.
For a finitely generated group $G = \langle S\rangle$ with a finite symmetric generating set $S$, the growth is defined by the function $n \mapsto |S^n|$, where $S^n$ is the set of elements resulting from the pointwise multiplication of $n$ copies of $S$. The growth rate is considered invariant (up to scaling) regardless of the choice of the symmetric generating set $S$.
Currently covered topics include:
The Mathlib.Analysis.Convex.Cone namespace contains results concerning convex cones that require a topology, a norm, or an inner product.
Use this module for analytic properties such as:
The mathlib4 build cache uses a trust-bounded delivery model. Because Lean can execute arbitrary code during elaboration, the cache cannot verify the byte-level integrity of artifacts. Instead, it uses a hierarchy of storage containers to ensure that artifacts produced at a specific trust level are only readable by consumers at that level or below.
| Container | Writer Identity | Trust Level |
|---|---|---|
master | master/staging branches, v4.* release tags | high |
forks | mathlib4 PR builds, non-master branches, bors try | medium |
nightly-testing | nightly-testing trusted branches | medium |
pr-toolchain-tests | nightly-testing experimental toolchain branches | low |
Consumers automatically look up artifacts in a specific order:
masternightly-testingmaster, forksThe Mathlib.Algebra.Notation subfolder provides definitions and minimal theory for fundamental algebraic operators. This includes:
0, 1+, -, *, /+ᵥ, •, -ᵥThese definitions are designed to be used very early in the import hierarchy of a project.
The Mathlib.Geometry.Convex namespace contains convexity results that are purely geometric and do not require a norm or an inner product.
If your work requires convexity results that depend on a norm or an inner product, use the Mathlib.Analysis.Convex namespace instead.
The Mathlib.Geometry.Convex.Cone namespace contains results regarding the algebraic theory of convex cones. These results are specifically designed for contexts that do not require a topology, a norm, or an inner product.
If your work requires topological results for convex cones, use the Mathlib.Analysis.Convex.Cone namespace instead.
Archive directory contains formalizations that do not have a clear place in the main mathlib repository, typically because they are niche or have very few dependencies within mathlib. These formalizations are maintained here to ensure they can be kept up to date as mathlib evolves.Mathlib/Geometry/Group directory contains formalizations related to geometric group theory, which studies finitely generated groups via their actions on geometric spaces. Currently, the library includes coverage for the growth of groups.The Archive/Wiedijk100Theorems directory contains Lean formalizations of theorems from Freek Wiedijk's 100 theorems list. These theorems are stored here because they do not fit naturally into the main mathlib hierarchy or other specialized Lean repositories.
To see which specific theorems from the list have already been formalized in Lean, visit the 100 Theorems documentation page.
The Mathlib.Analysis.Convex namespace contains convexity results that specifically require a norm or an inner product.
If you are looking for convexity results that do not require a norm or an inner product, use the Mathlib.Geometry.Convex folder instead.
The Penrose diagram implementation uses three specific file types to define and render diagrams:
.dsl): Define the objects available within a specific domain..sty): Specify the visual rules and how objects from a domain should be drawn..sub): Describe the actual content and structure of specific diagrams.These diagrams are rendered in the Lean infoview via ProofWidgets4.