Referencing Theorems in Mathlib in an Academic Paper

Stream: mathlib4

[Fred Rajasekaran]

Has there been any consensus on how to cite a result in mathlib in a math paper?

I'm wrapping up a paper on lattice Yang-Mills theories, and in it we use some very basic facts about Lie groups and Lie algebras. These facts are standard and don't need to be attributed to a single person, e.g. the Lie algebra of a direct product of Lie groups is the direct sum of the Lie algebras, the Haar probability measure on a product of Lie groups is the product of the Haar measures, etc. Since the paper will likely end up in a probability journal, we decided it would be a good idea to put references for these statements since some readers won't have experience with the concepts (we also didn't directly include the proofs in our paper since we wanted the paper to be shorter).

I was able to find them in Bourbaki and included that as a reference, but since mathlib is supposed to be a math library, I was wondering if there is a standard way of citing theorems from it (particularly for facts such as the ones above that don't need to be attributed an author).

I also understand it's probably best to cite a book on the subject for pedagogical reasons, but I'm still curious how to cite mathlib if I ever need to.

[Eric Wieser]

When I did this in the past, I gave a github permalink to a line of code in mathlib, and explained that all links formatted in a certain way were from mathlib.

[Heather Macbeth]

Fred Rajasekaran said:

we use some very basic facts about Lie groups and Lie algebras. These facts are standard and don't need to be attributed to a single person, e.g. the Lie algebra of a direct product of Lie groups is the direct sum of the Lie algebras, the Haar probability measure on a product of Lie groups is the product of the Haar measures, etc.

In my opinion, there's still something to attribute there. For example, if you are using the "Lie group" object in mathlib, I would give attribution to the PR which introduced Lie groups: !3#3529. I would put this in a footnote, also including Nicolo's name as the author of this PR.

In an article, I tend to do this for the 3-10 most important mathlib contributions which are prerequisite for my work. If the PR author happens to have written an article about their work then I would cite that instead (for example, Floris wrote an article about his Haar measure contribution, so you could cite that instead of footnooting the PR in which he introduced it, same for Oliver's article about Lie algebras).

[Eric Wieser]

Heather Macbeth said:

I would put this in a footnote, also including Nicolo's name as the author of this PR.

In my thesis, I additionally attributed the reviewers; often they are much closer to co-authors than they would be in an academic review.

[Eric Wieser]

If you're interested I can share some .bib files with every mathlib PR (lean3 + lean4) up to March 2024...

[Riccardo Brasca]

You can have a look at how this is done in the Annals of Formalized Mathematics.