Documentation: citations/bibliography

Stream: new members

[Kevin Kappelmann]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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]

There's a Lean+LaTeX thread here somewhere

[Patrick Massot]

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]

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]

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]

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

[Patrick Massot]

where you can show Lean code by clicking on text

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Kappelmann]

Damn, that's pretty nice! :fire:

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Patrick Massot]

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]

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

[Kevin Buzzard]

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]

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]

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]

You should also cite Taylor-Wiles though ;-)

[Kevin Kappelmann]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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.