Reference textbook in lemmas

Stream: general

[Yaël Dillies]

There's a handful of lemmas in mathlib that are direct translations of textbook lemmas. Should we have a @[textbook the_textbook_it_comes_from] attribute to mark them as such and collect them somewhere on the website?

[Eric Wieser]

Or should we do the reverse using the design ofundergrad.yml, and reference textbook lemmas from a yaml file (per textbook?)

[Yaël Dillies]

Could also do, but the problem is that those tend to fall behind mathlib.

[Eric Wieser]

undergrad.yml isn't allowed to fall out of sync

[Eric Wieser]

CI fails if the lemmas it refers to disappear

[Yaël Dillies]

Mostly, the information isn't there in the file when you read it

[Eric Wieser]

Well, the information in the textbook isn't there in the lean file either

[Yaël Dillies]

Okay, let me finish my sentence and then you can speak again

[Yaël Dillies]

Whichever way we pick, that would have the advantage of uncluttering docstrings (which could do without that information) and (in the attribute version) uniformly mark such textbook lemmas within the files. Further, it would be a way to link back and forth in a textbook translation, or even generate the textbook translation from more mathlib-style files.

[Yaël Dillies]

I guess Eric's solution has the advantage of reusing existing parts.

[Eric Wieser]

The yaml file could be replaced with a dsl of some kind in lean4, that repeated the statements

[Yaël Dillies]

The problem I see with this yaml approach is that the information disappears from the file in question. Maybe we can solve that by having doc-gen generate a link back to the yamls a file belongs to?

[Eric Wieser]

I think it's ok for the information to be missing from the source, but doc-gen should certainly show these cross-links

[Eric Wieser]

(I think doc-gen4 struggles to show attributes a lot of the time anyway)

[Kyle Miller]

Do we have any sort of way to create special markdown link extensions? Like "This lemma is [rudin1953 Theorem 2.2].", and then there'd be a reference link in the docstring, and the references page could have backlinks.

[Eric Wieser]

Yes, but:

• Doing it in mathlib3 likely involves switching to a more sane markdown package in doc-gen. I made a start on this a while back, but...
• Doing it in mathlib4 requires modifying the markdown parser written in Lean, which is unrelated to any work spent above.

[Kyle Miller]

Don't we actually already have something that's very close to this in the form of library notes?

[Eric Wieser]

Using a loose interpretation of the word "textbook", another answer is to just create third-party projects like https://github.com/eric-wieser/lean-matrix-cookbook that contain the statement of every lemma in the textbook, and try to prove it with as short a lean expression as possible. Then a custom webpage could present this in a useful way

[Eric Wieser]

This also captures things like "this is a generalization of [textbook result], by showing precisely what the special case looks like"

[Eric Wieser]

Kyle Miller said:

Don't we actually already have something that's very close to this in the form of library notes?

I think there's very little value to building new features into doc-gen3. I don't think doc-gen4 supports library notes yet, but I haven't checked recently

[Kyle Miller]

I think my point here is that we can record that a given lemma is a textbook lemma by representing it in the docstring, and a technical implementation for indexing is more of a nice touch than a must-have.

[Yaël Dillies]

One of goals is to remove that information from the docstring and get it somewhere else, because it's unhelpful when you try to use a lemma.

[Eric Rodriguez]

I think I'd prefer the attribute to yaml files; I get that docgen can parse it, but if you're trying to understand the proof you're likely in source view, and being told "oh this is in Washington" would be really nice

[Kyle Miller]

Yaël Dillies said:

because it's unhelpful when you try to use a lemma.

How do you mean? Are you saying it actively impedes using a lemma somehow if it's mentioned in the last line of a docstring?

[Yaël Dillies]

I guess I like uniformity :stuck_out_tongue:

[Yaël Dillies]

Eric Wieser said:

Using a loose interpretation of the word "textbook", another answer is to just create third-party projects like https://github.com/eric-wieser/lean-matrix-cookbook that contain the statement of every lemma in the textbook, and try to prove it with as short a lean expression as possible. Then a custom webpage could present this in a useful way

The thing is that those third-party projects have less visibility than if they were hosted on mathlib. It would be great if we could have all the textbook formalisations gathered somewhere on the mathlib website, and possibly even have them be parts of mathlib.

[Pedro Sánchez Terraf]

Kyle Miller said:

How do you mean? Are you saying it actively impedes using a lemma somehow if it's mentioned in the last line of a docstring?

Nice idea, keeping “formalizer's hints” at the top, and further info (like references) at the bottom.

[Kyle Miller]

In some IDE frontends, there's a distinction also between the short form of a docstring and the long form. The short form is what you see if you mouse over an identifier. For example, the Qt C++ documentation style has a \brief command for the short form (link). Just bringing this up since it's something worth thinking about if the complaint is long docstrings.

[Moritz Doll]

One downside of an attribute might be that it makes it harder to generate the 'book-to-mathlib' list in the correct order.

[Scott Morrison]

My preference would be to encourage more of these "links", and to have them be as close to the source code as possible. They are very helpful to readers!

[Eric Wieser]

Another downside of the attribute is that if a lemma is removed there's not obvious obligation to find something else to move the attribute to; whereas if there's a yaml file (or DSL) then you have to think of something else to fill the gap

[Eric Wieser]

I assume that whatever reason we chose for avoiding an attribute-based approach in undergrad.yml can be applied to the case of textbooks too

[Moritz Doll]

Is there a possibility to have not a yaml file but a lean file for each book and all the references for a particular lemma is then displayed in the info-view? (maybe this is Eric's dsl idea?)

[Eric Wieser]

I don't really know where the info view would show this stuff, since it shows tactic state not lemma information

[Eric Wieser]

But yes, I'm imagining that a textbook is going to have results which are either:

• Exactly the version in mathlib
• A trivial specialization of a result in mathlib
• A consequence of a short series of lemmas in mathlib

The attribute approach doesn't distinguish the top two cases and can't handle the third

[Eric Wieser]

A .lean file could have markers for each of these cases (or deduce them from the proof syntax), and show them appropriately

[Yaël Dillies]

Both approaches aren't mutually exclusive, right?

[Alex J. Best]

But would you really want a yaml file listing every lemma of a bunch of randomly chosen textbooks? The idea of the undergrad file is to track progress with the slightly vague goal of formalizing an undergraduate curriculum. When formalizing textbook lemmas the goal is most often not for completeness (as everyone here knows formalization dictates that things be set up in a very different way to a textbook presentation), but rather to provide cross references with the informal literature. Personally I'm a fan of doing this in docstrings (maybe with some fixed syntax so the relevant info can be extracted if needed).

[Yaël Dillies]

I want the attribute in the case where we are formalising some lemmas from a specific chapter of some textbook among other mathlib theory files. yaml files or recap lean files are instead perfect when you're exhaustively formalising a textbook.