mathlib
swMATH ID: | 36839 |
Software Authors: | van Doorn, Floris; Ebner, Gabriel; Lewis, Robert Y.; The mathlib Community |
Description: | Maintaining a library of formal mathematics. The Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors and to lessen the burden of reviewing contributions, we have developed a number of tools for the library which check proof developments for subtle mistakes in the code and generate documentation suited for our varied audience. |
Homepage: | https://leanprover-community.github.io |
Source Code: | https://github.com/leanprover-community/mathlib |
Keywords: | formal mathematics; library development; linting |
Related Software: | Lean; Coq; Isabelle/HOL; GitHub; Archive Formal Proofs; Agda; Mizar; PVS; Coquelicot; Isabelle; hierarchy-builder; Metamath; Flyspeck; Mathematical Components; HOL Light; Nuprl; Minkowskis_Theorem; PARI/GP; Gaussian_Integers; KANT/KASH |
Cited in: | 32 Documents |
Standard Articles
1 Publication describing the Software, including 1 Publication in zbMATH | Year |
---|---|
Maintaining a library of formal mathematics. Zbl 1455.68262 van Doorn, Floris; Ebner, Gabriel; Lewis, Robert Y. |
2020
|
all
top 5
Cited by 67 Authors
all
top 5
Cited in 7 Serials
all
top 5