Maintaining a Library of Formal Mathematics
Programming Languages
2020-07-28 v2 Mathematical Software
History and Overview
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.
Cite
@article{arxiv.2004.03673,
title = {Maintaining a Library of Formal Mathematics},
author = {Floris van Doorn and Gabriel Ebner and Robert Y. Lewis},
journal= {arXiv preprint arXiv:2004.03673},
year = {2020}
}
Comments
To appear in Proceedings of CICM 2020