You can cite mathlib using the following BibTeX entry:
@InProceedings{ mathlib2020,
author = {The mathlib Community},
title = {The Lean Mathematical Library},
year = {2020},
isbn = {9781450370974},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3372885.3373824},
doi = {10.1145/3372885.3373824},
booktitle = {Proceedings of the 9th ACM SIGPLAN International
Conference on Certified Programs and Proofs},
pages = {367-381},
numpages = {15},
keywords = {formal proof, formal library, Lean, mathlib},
location = {New Orleans, LA, USA},
series = {CPP 2020}
}The mathlib project is actively maintained and updated. In the interest of reproducibility, you may want to manage your code's dependency on mathlib using the leanproject command-line tool. This will help ensure others can retrieve the right version of mathlib for your project.
Lean was introduced in the paper "The Lean Theorem Prover", by de Moura et al., which you can cite using:
@InProceedings{ demoura2015lean,
author = {de Moura, Leonardo and Kong, Soonho and Avigad, Jeremy and
van Doorn, Floris and von Raumer, Jakob},
editor = {Felty, Amy P. and Middeldorp, Aart},
title = {The Lean Theorem Prover (System Description)},
booktitle = {Automated Deduction - CADE-25},
year = {2015},
publisher = {Springer International Publishing},
address = {Cham},
pages = {378--388},
isbn = {978-3-319-21401-6}
}