Skip to content

Latest commit

 

History

History
43 lines (37 loc) · 1.88 KB

CITATION.md

File metadata and controls

43 lines (37 loc) · 1.88 KB
Raw

Citing Mathlib

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}
}