Citing lean + mathlib

Stream: general

[Adam Topaz]

Does anyone have a "standard" bibtex entry that they use for citing mathlib?
I quickly came up with the following:

@misc{mathlib,
author = {Mathlib Contributors},
title = {Lean mathlib},
year = {2022},
publisher = {GitHub},
journal = {GitHub Repository},
howpublished = {https://github.com/leanprover-community/mathlib}
}

What about citing Lean itself? Do the Lean devs have a preference for how we should cite Lean3 in papers?

[Adam Topaz]

Also, should we post these bibtex entries somewhere on github and/or the community webpage?

[Bolton Bailey]

See this previous discussion

[Adam Topaz]

Perfect! Thanks

[Kevin Buzzard]

I'm pretty sure that there's also a standard lean citation, check out the perfectoid paper maybe or the mathlib paper?

[Adam Topaz]

yeah I'll probably use the one from the mathlib paper.

[Leonardo de Moura]

What about citing Lean itself? Do the Lean devs have a preference for how we should cite Lean3 in papers?

Thanks for asking. For Lean 3, the standard reference is
https://link.springer.com/chapter/10.1007/978-3-319-21401-6_26#citeas
For Lean 4, https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37#citeas

[Adam Topaz]

Great! Thanks so much @Leonardo de Moura !

[Eric Wieser]

@Adam Topaz, what bibtex did you end up using for the mathlib citation? If there's consensus on it, we should commit it to the mathlib repo

[Adam Topaz]

@inproceedings{10.1145/3372885.3373824,
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}
}

and

@InProceedings{10.1007/978-3-319-21401-6_26,
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"
}

for the Lean3 citation.

Note that I removed the "abstract" field in both cases which was included when I originally downloaded the entry.

[Adam Topaz]

If you click on the little "quote" icon here: https://dl.acm.org/doi/10.1145/3372885.3373824 then you will get the full bibtex entry

[Adam Topaz]

Should we add a CITATION.cff file, or just mention the bibtex on the README.md?

[Eric Wieser]

We should add a CITATION.md file, which still gets special github support; but also lets us add instructions like "we recommend you also cite Lean"

[Bolton Bailey]

Has anyone used GitHub's .md support before? Does the .md file have to be in a particular format to get support? Or will it just recognize the first BibTex entry it sees in the file?

[Eric Wieser]

Nothing as clever, it just puts a citation link in the sidebar that links to the MD file

[Bolton Bailey]

I definitely like the idea of having a visible way of citing mathlib as a convenience to those writing papers based on it, so I made PR #17202. Everyone feel free to voice objections or comments.