## Stream: new members

### Topic: Documentation: citations/bibliography

#### Kevin Kappelmann (Apr 16 2019 at 08:12):

Hi, is there any standard way to include citations/have some kind of bibliography in Lean? That is, when I am formalising a theory/theorem and I want to leave some explaining words for the reader and references to the literature, what is the right way to do this in Lean?
Also slightly more general: are there any best practices for documenting one's formalisations?

#### Kevin Buzzard (Apr 16 2019 at 08:15):

Mathlib does not really have many comments in, and this has always been a source of some sadness to me. However there are some. There are sometimes a bunch of comments in between /- and -/ in mathlib files with references. I'll dig one out for you.

#### Kevin Buzzard (Apr 16 2019 at 08:16):

https://github.com/leanprover-community/mathlib/blob/361e216388d6d63e12f2cb11a444fce3c05701d9/src/topology/basic.lean#L1

#### Kevin Buzzard (Apr 16 2019 at 08:16):

That's way more than average. Compare with Coq, where many of the files I've looked at seem to have a huge comment at the top explaining what is going on.

#### Kevin Buzzard (Apr 16 2019 at 08:18):

I am trying to copy the Coq philosophy in my work, e.g. https://github.com/leanprover-community/lean-perfectoid-spaces/blob/4d4746673c88730987a3a1a93614ad5f8a73144c/src/valuation/basic.lean#L12 , but there are still plenty of files in that repo that don't have extensive documentation (sometimes because they are not quite finished, but often because we've not got around to it yet).

#### Patrick Massot (Apr 16 2019 at 08:24):

Let me try a clearer message: @Kevin Kappelmann currently this aspect of mathlib is a disaster. Please do your best to document what you are doing, and include as many references to actual books or paper as you can in the comments. Everybody will be grateful

#### Kevin Kappelmann (Apr 16 2019 at 08:26):

Thank you Kevin & Patrick. So basically, there is no standard yet if I understand correctly.
I am quite concerned about lacking explanations and references in ITPs, but it does not seem a priority for most people I have spoken to so far. I would really like to have an understandable library of mathematical knowledge rather than a huge collection of opaque proofs; for otherwise, I see problems arising in the near future, in particular concerning search and automation.

#### Kevin Buzzard (Apr 16 2019 at 08:26):

Yes -- make your own rules, and show the community how it can be done. Put extensive comments wherever you think is best. Let's change the status quo.

#### Kevin Buzzard (Apr 16 2019 at 08:27):

Patrick has done some spectacular work enabling you to write Lean files with LaTeX comments, and the LaTeX comments are displayed in LaTeX in a browser.

#### Kevin Kappelmann (Apr 16 2019 at 08:27):

Patrick has done some spectacular work enabling you to write Lean files with LaTeX comments, and the LaTeX comments are displayed in LaTeX in a browser.

That sounds great. Where can I read more about this?

#### Kevin Buzzard (Apr 16 2019 at 08:28):

A PhD student at Imperial, @Mohammad Pedramfar , is working on getting a local install of Lean in a browser to make this even better -- people might be able to edit code live.

#### Kevin Buzzard (Apr 16 2019 at 08:28):

There's a Lean+LaTeX thread here somewhere

#### Patrick Massot (Apr 16 2019 at 08:28):

I should point out that some people already try to change that: have a look at proof comments in https://github.com/leanprover-community/mathlib/pull/900/files (although I wish @Sebastien Gouezel could also include a reference to the book he is following)

#### Kevin Buzzard (Apr 16 2019 at 08:29):

http://pat.perso.ens-lyon.org/M1P1/ is an example of Patrick's work. Click on the grey squares to see the Lean state at that point.

#### Patrick Massot (Apr 16 2019 at 08:29):

There are various results one can achieve. The link indicated by Kevin is when you ask to see only the math and tactic state

#### Patrick Massot (Apr 16 2019 at 08:30):

https://www.math.u-psud.fr/~pmassot/lean/ is another style

#### Patrick Massot (Apr 16 2019 at 08:30):

where you can show Lean code by clicking on text

#### Kevin Buzzard (Apr 16 2019 at 08:31):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20.2B.20LaTeX.3F/near/156681378 is a history of the project. You'll find a link to Patrick's repo in there I'm sure

#### Patrick Massot (Apr 16 2019 at 08:31):

https://www.math.u-psud.fr/~pmassot/enseignement/math114/cours4.html is using yet another layout, with prominent Lean code

#### Kevin Buzzard (Apr 16 2019 at 08:31):

All of this is done by simply writing LaTeX comments as comments within the Lean code and using a clever python script.

#### Patrick Massot (Apr 16 2019 at 08:31):

Note that I added support for commutative diagrams using tikzcd a few days ago

#### Kevin Buzzard (Apr 16 2019 at 08:32):

Did you announce that and I missed it, or are you just announcing it now? Is this because of your teaching?

#### Kevin Kappelmann (Apr 16 2019 at 08:32):

Damn, that's pretty nice! :fire:

#### Kevin Buzzard (Apr 16 2019 at 08:33):

I have this idea of writing some introductory analysis "textbook" in formally verified Lean + LaTeX

#### Kevin Buzzard (Apr 16 2019 at 08:34):

but it's on a big pile of ideas which I have for this software

#### Kevin Buzzard (Apr 16 2019 at 08:34):

Until then, liberally sprinkle comments through your code and feel free to write some in LaTeX :D

#### Patrick Massot (Apr 16 2019 at 08:37):

Did you announce that and I missed it, or are you just announcing it now? Is this because of your teaching?

I didn't announce it. It comes from my teaching of course. But I'm horribly late in everything I have to do, including grading stuff and writing lecture notes

#### Patrick Massot (Apr 16 2019 at 08:37):

I did quotients last week, so I badly needed commutative diagrams

#### Kevin Buzzard (Apr 16 2019 at 08:38):

It is great that teaching is guiding the development of this project. It makes it a more complete project -- it somehow guarantees usefulness.

#### Kevin Kappelmann (Apr 16 2019 at 08:51):

Is it a good idea to do something like this:

/-- The famous proof of Fermat's last theorem following /cite{wiles1995modular}. -/
theorem fermats_last_theorem (a b c n: ℕ+) : n>2 → a^n + b^n ≠ c^n := sorry

-- The bibliography
/-
\begin{filecontents}{bibliography.bib}
@article{wiles1995modular,
title={Modular elliptic curves and Fermat's last theorem},
author={Wiles, Andrew},
journal={Annals of mathematics},
volume={141},
number={3},
pages={443--551},
year={1995},
publisher={JSTOR}
}
\end{filecontents}
-/


?

#### Kevin Buzzard (Apr 16 2019 at 08:53):

That's the sort of thing that, were Patrick not teaching so much at the time, he could just edit his python script to handle in about 20 minutes :-)

#### Kevin Buzzard (Apr 16 2019 at 08:53):

You should also cite Taylor-Wiles though ;-)

#### Kevin Kappelmann (Apr 16 2019 at 08:55):

Haha, I, unsurprisingly, am not gonna formalise this particular theorem as my first project :D

#### Kevin Buzzard (Apr 16 2019 at 08:55):

mathscinet spits out

@article {MR1333035,
AUTHOR = {Wiles, Andrew},
TITLE = {Modular elliptic curves and {F}ermat's last theorem},
JOURNAL = {Ann. of Math. (2)},
FJOURNAL = {Annals of Mathematics. Second Series},
VOLUME = {141},
YEAR = {1995},
NUMBER = {3},
PAGES = {443--551},
ISSN = {0003-486X},
MRCLASS = {11G05 (11D41 11F11 11F80 11G18)},
MRNUMBER = {1333035},
MRREVIEWER = {Karl Rubin},
DOI = {10.2307/2118559},
URL = {https://doi.org/10.2307/2118559},
}


for the Wiles paper

#### Patrick Massot (Apr 16 2019 at 08:56):

You don't need the filecontents lines. The day a script will generate documentation from mathlib it will handle this. I do think that include BibTeX entries like this is useful. Even without any computer parsing it will help readers. And it can't do any harm

#### Kevin Buzzard (Apr 16 2019 at 08:56):

Haha, I, unsurprisingly, am not gonna formalise this particular theorem as my first project :D

Maybe you could do the Langlands--Tunnell theorem as your first project then; I think it's all downhill from there.

#### Kevin Kappelmann (Apr 16 2019 at 09:00):

Haha, I, unsurprisingly, am not gonna formalise this particular theorem as my first project :D

Maybe you could do the Langlands--Tunnell theorem as your first project then; I think it's all downhill from there.

by simp [langlands_tunnell] you say?

#### Kevin Buzzard (Apr 16 2019 at 09:08):

Well, once the AI community has got better theorem provers (give then ten years, so I heard last week at AITP) then that should work fine :-)

#### Neil Strickland (Apr 16 2019 at 09:19):

I think that there is a great need for standards in this area. Perhaps the Formal Abstracts people will propose some relevant standards, but there does not seem to be anything useful at https://github.com/formalabstracts as yet. I also think that metadata should be accessible to Lean, to enable better search tools. Perhaps we could implement something like this?

/-
import metadata

...

theorem fermats_last_theorem : ...

fermats_last_theorem.references := [
{key := "MR1333035", comment :="This is the original paper"},
{key := "MR1605709", comment := "This is the book"}
]

fermats_last_theorem.keywords := ["Fermat","Diophantine equations"]

-/


#### Rob Lewis (Apr 16 2019 at 09:20):

If and when we start to put real metadata into mathlib, there's no reason to keep it as plain text comments. We should be able to tag theorems with their source, author, etc. in a semantically meaningful way. Then we could e.g. write a program that retrieves all theorems in mathlib coming from Atiyah-Macdonald.

#### Rob Lewis (Apr 16 2019 at 09:21):

We were experimenting with this at the very start of the formal abstracts project. I'm not sure what they're using now.

#### Sebastien Gouezel (Apr 16 2019 at 09:24):

I should point out that some people already try to change that: have a look at proof comments in https://github.com/leanprover-community/mathlib/pull/900/files (although I wish Sebastien Gouezel could also include a reference to the book he is following)

Not following any book, sorry, this is just the standard natural proof.

#### Jesse Michael Han (Apr 16 2019 at 17:00):

It's not hard to write a custom user attribute which lets you associate strings (DOI, MSC code, etc) to theorems and definitions. Something like this is in formalabstracts/master, but we haven't really used it.

#### Koundinya Vajjha (Apr 16 2019 at 19:27):

We are currently working out this very issue in Formal Abstracts. We've gotten in touch with Pieter Belmans of the Stacks project and Kerodon he has kindly allowed me to use his TeX renderer to produce webpages, with specified tags. The idea is that these tags then become central references for citation purposes and the like. Progress is slow as I have a very busy summer ahead but I would tentatively say sometime later in the year for a service which users can contribute to.

#### Kevin Buzzard (Apr 16 2019 at 19:32):

This is great news. Don't rush it -- get it right :-) All this Lean code is quite intimidating for mathematicians, but FAbstracts needs to be quite the opposite: we want mathematicians to _use_ it!

#### Koundinya Vajjha (Apr 16 2019 at 19:33):

As Jesse said, the linking between the formal text and the informal text would then be acheived through the fabstracts user attribute with a tag parameter. We could add many more bells and whistles to the service such as inline code snippets, a comments app for each tag, user authorization etc.

#### Koundinya Vajjha (Apr 16 2019 at 19:54):

I also think that metadata should be accessible to Lean, to enable better search tools. Perhaps we could implement something like this?

A lean function to extract metadata from a declaration is in
https://github.com/formalabstracts/formalabstracts/blob/master/src/tactic/metadata.lean
we also have a function to dump this metadata (for [@fabstract]-marked declarations) into JSON.

Last updated: May 06 2021 at 22:13 UTC