@inproceedings{mathlib2020lean,
title = {The Lean Mathematical Library},
author = {{The mathlib Community}},
year = {2020},
date = {2020-01-20},
isbn = {978-1-4503-7097-4},
doi = {10.1145/3372885.3373824},
url = {https://doi.org/10.1145/3372885.3373824},
urldate = {2020-07-11},
booktitle = {Proceedings of the 9th {{ACM SIGPLAN International
Conference}} on {{Certified Programs}} and {{Proofs}}},
series = {{{CPP}} 2020},
pages = {367--381},
publisher = {{Association for Computing Machinery}},
keywords = {formal library,formal proof,Lean,mathlib},
abstract = {This paper describes mathlib, a community-driven effort to
build a unified library of mathematics formalized in the
Lean proof assistant. Among proof assistant libraries, it
is distinguished by its dependently typed foundations,
focus on classical mathematics, extensive hierarchy of
structures, use of large- and small-scale automation, and
distributed organization. We explain the architecture and
design decisions of the library and the social organization
that has led to its development.},
location = {{New Orleans, LA, USA}}
}