Adding books to the library

Stream: general

[Ali Hadizadeh Moghadam]

Hi. I was wondering if you'd think it's a good idea to add definitions and theorems book by book (i.e., write down everything from the famous reference X in the field Y)?

I think it would help mathematicians in the future use their desired lemmas. For instance, you could open up the book, find the lemma you need, and then look up its Lean equivalent on the database, according to a naming convention, or maybe just by browsing through the library repo.

(Searched; didn't find similar earlier discussion.)

[Mario Carneiro]

This style is used in metamath, and I am quite fond of it, but I think it is not standard in mathlib. There are lots of people I know asking for better cross references between formal libraries and informal sources, and I think we should try to collect as much of this kind of information as people are willing to contribute

[Kyle Miller]

If you search for "formalize textbook" you can find a few discussions. I think its a good idea — what I want to see is definitions and theorems written in a way that relies on Mathlib as much as possible. That way it serves as a "rosetta stone" between the language of the textbook and the language of Mathlib. Some of these projects could be in the Mathlib/Archive folder.

[Yaël Dillies]

This has already been discussed at length before

[Mario Carneiro]

What I meant was something a little different: you put on the mathlib theorem itself, in the doc comment, a reference to the corresponding theorem in famous textbook X. (I'm aware that there is almost never a perfect match here, so you interpret "corresponding" in a loose way so as to have something to cite.)

[Kyle Miller]

A reason I like the other direction is that there's no need for it to be a loose match. It's giving you the important information about how to glue together the "textbook API" to the "mathlib API", and someone who's refactoring a theorem doesn't need to read the cited textbook to make sure they're not changing it beyond all recognition — they just have to make sure the textbook formalization still builds.

[Kyle Miller]

These approaches aren't mutually exclusive of course.

[Ali Hadizadeh Moghadam]

Kyle Miller said:

If you search for "formalize textbook" you can find a few discussions.

Found a good related thread in #mathlib4 > Project idea: linking MathLib to math books. I'll start reading it. We can close this thread if you feel like this is an unnecessary duplicate (or whatever the Zulip practices dictate; I'm a newbie).

[Mario Carneiro]

Having the textbook rosetta approach is useful, but I don't think it's a replacement for citations on theorems, because it's less discoverable than having it on the theorem itself. For example you might notice that you are seeing a lot of theorems with EGA references and think "maybe I should read EGA"

[Ruben Van de Velde]

Why not both?

[Ruben Van de Velde]

Anyway, it seems like this hasn't got further than talk on zulip because people lack time

[Mario Carneiro]

also the textbook rosetta approach seems more heavyweight, like it would be weird to do that for just one theorem, while adding just one citation to a theorem seems fine

[Frédéric Dupuis]

Maybe we should explicitly encourage textbook citations in theorem docstrings somewhere. I've been tempted to do this before, but then ended up putting the citations in the module docstring because it felt out of place on the theorem itself since we basically never do it.

[Mario Carneiro]

another aspect of the metamath approach that makes this a bit less onerous: there is a short linking style like [EGA II], and then the target of this reference is defined in a bibliography page that has more detail on all the references

[Mario Carneiro]

(less onerous and also more consistent and easier for automated tools to scrape)

[Mario Carneiro]

this is also used to power more views in the docgen that list all citations in the order they appear in the reference, making it a very low effort version of the textbook rosetta idea

[Ali Hadizadeh Moghadam]

Kyle Miller said:

Some of these projects could be in the Mathlib/Archive folder.

That's great!

I'm not very sharp in making conclusions, so sorry for asking: is it officially ok to fill the Archive folder with these things? (I know there are routines for contribution)

I looked up the mentioned thread, and it seems every one was happy, but I didn't find any signs of "ok whoever does book x theorem y please let us know so that we'll put it in repo folder z".

[Yaël Dillies]

Just open a PR and we'll see what we think! Personally, I see it as suitable for inclusion in archive

[Yaël Dillies]

Ruben Van de Velde said:

Anyway, it seems like this hasn't got further than talk on zulip because people lack time

... yep. I might have time this summer to give a good shot at making LeanCamCombi do what it actually set out to do

[Ali Hadizadeh Moghadam]

Ruben Van de Velde said:

Anyway, it seems like this hasn't got further than talk on zulip because people lack time

Well, I've been talking to my prof to host a REU on formal proof. If it goes well, I was precisely planning to feed the victims with a textbook formalizing project. So, maybe that'd help fuel up this discussion again.

[Ali Hadizadeh Moghadam]

Yaël Dillies said:

Just open a PR

Well that's great! Thanks!

I'll let my prof know the community has this inclination.

[Ali Hadizadeh Moghadam]

BTW, if Lean REU (Research Experience for Undergrads) seems a tasty topic, I can open another thread for it. Personally, I'm really eager to know your suggestions (textbooks to start with, best practices, ...)

[Kim Morrison]

No new idea under the sun -- we had this in Mathlib3, see docs/tutorial/representation_theory/etingof.lean, which was the beginning of following Etingof's great and free book.

Unfortunately it was not ported to Mathlib 4. If anyone would like to do that, and/or continue, that would be lovely!

[Mario Carneiro]

(note that if it had been done as citations in docstrings, it would have been ported!)

[Kyle Miller]

(note that these aren't mutually exclusive kinds of artifacts and they each have their benefits!)