Maintaining a Library of Formal Mathematics
Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 kernel pith:37XF6EG5record.jsonopen to challenge →
classification
cs.PL
cs.MSmath.HO
keywords
librarydevelopedaudiencebackgroundsbarrierburdencheckcode
read the original abstract
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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.