diff --git a/CITATION.md b/CITATION.md
new file mode 100644
index 0000000000000..32d35af3bb51e
--- /dev/null
+++ b/CITATION.md
@@ -0,0 +1,43 @@
+
+# Citing Mathlib
+
+You can cite `mathlib` using the following BibTeX entry:
+
+```bib
+@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`](https://leanprover-community.github.io/leanproject.html) 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"](https://www.semanticscholar.org/paper/The-Lean-Theorem-Prover-(System-Description)-Moura-Kong/2a441a46e228ed0ea2251a4e61be6c7025b45766), by de Moura et al., which you can cite using:
+
+```bib
+@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}
+}
+```
diff --git a/docs/references.bib b/docs/references.bib
index f52e984a5f582..4fb1ecbef57f8 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -574,6 +574,19 @@ @InProceedings{   deligne_formulaire
   mrreviewer    = {Jacques Velu}
 }
 
+@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}
+}
+
 @Article{         dold1958,
   author        = {Dold, Albrecht},
   title         = {Homology of symmetric products and other functors of
@@ -1379,7 +1392,25 @@ @Article{         markowsky1976
   author        = {Markowsky, George},
   year          = {1976},
   month         = {Dec},
-  pages         = {53–68}
+  pages         = {53-68}
+}
+
+@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}
 }
 
 @InProceedings{   mcbride1996,