Named Theorems

Stream: general

[Hunter Monroe]

Could we establish a convention that "named theorems" for instance "Bézout's lemma" be distinguished by bolding the name in the theorem/lemma doc string, that is "Bézout's lemma" or "triangle inequality"?

[Bryan Gin-ge Chen]

I like that idea!

[Eric Wieser]

Can we do better semantically? @[known_as "triangle inequality"]?

[Eric Wieser]

I mean I guess doc-gen can parse out the bold anyway

[Bryan Gin-ge Chen]

Certainly it'd be nice if doc-gen could collect a list of named results from Lean code. In the meantime I think bolding names in doc strings will be simple and helpful.

[Bryan Gin-ge Chen]

(PR at #8182).

[Mario Carneiro]

regarding bezout's lemma specifically, I have failed to find it more than once because I always forget the symbol reading name of the lemma, and grep fails because there are no text hits for "bezout" in mathlib (because of the accent)

[Mario Carneiro]

I would really like the name to be just nat.bezout or nat.bezout_lemma

[Eric Wieser]

Is it worth having a special type of alias here such that the linter warns if the aliased name is actually used?

[Eric Wieser]

That way we can have aliases for finding lemmas, but can elect one as the canonical spelling

[Johan Commelin]

Mario Carneiro said:

I would really like the name to be just nat.bezout or nat.bezout_lemma

Wow! I've always heard you arguing for the naming convention, and against ad hoc "wellknown theorem names named after random mathematician".

This remark was a surprise to me :grinning: :rofl: :crazy:

[Mario Carneiro]

Scroll up in this thread, I say something similar earlier

[Johan Commelin]

Wow, that was from before I even joined zulip...

[Anatole Dedecker]

I really like the semantic idea of Eric. Maybe doc-gen could even automatically add them to the tags of the file to make finding them easier

[Damiano Testa]

Johan, I had no idea that there was a time when you were not on Zulip! I've learned so much today! :wink:

[Patrick Massot]

Johan is a newbie, he didn't experience the gitter chat.

[Hunter Monroe]

OK, the PR for bolding named theorems was accepted into mathlib (my first!). Do we need to do the same for definitions, which would allow the creation of an index of standard math concepts using their normal names?

[Johan Commelin]

@Hunter Monroe I guess that most mathlib definitions already use "normal names" quite closely. (E.g., a ring is a ring and a topological space is a topological_space.) So probably there is less direct benefit there. Do you have particular definitions in mind where you would want to apply this?

[Hunter Monroe]

@Johan Commelin there is a need for a far more comprehensive auto-generated index of definitions and theorems covered in mathlib, with their conventional names not the mathlib names, than provided on the overview page, which would: (1) be more thorough, for instance, by including probability concepts (present in the undergrad page but not the overview page), and (2) by being thorough, would make it obvious from a glance what is not covered, for instance, random variables, expected value, central limit theorem). Mathlib has outgrown the manually maintained overview and undergrad pages. The documentation does not fill this need, for instance, see the search results for probability.

[Johan Commelin]

@Hunter Monroe The fact that probability concepts are missing on the overview is because nobody added them! Please make a PR!

[Johan Commelin]

I think manually maintained lists will be probably stay around for a while.

[Johan Commelin]

It's usually a human judgment to decide what deserves to be on a list or not.

[Johan Commelin]

Although it might be possible to decentralize this. We could have an attribute @[overview "Human readable thm name"] before definitions/theorems that we want to include in the list.

[Hunter Monroe]

OK but the same shortcoming applies to graph theory, where it takes a good deal of work to determine that simple graphs are covered but not subgraphs and homomorphisms, and likewise for every other field of mathematics. Just as with theorems, bolding the name within the docstring could flag these for inclusion in auto-generated index--providing the human judgment.

[Bryan Gin-ge Chen]

I think we should use a custom attribute to detect the human generated names; just searching for bolded strings won't be reliable.

[Hunter Monroe]

If you do a search of mathlib in VS code for " **", there is hardly any extraneous stuff that would have to be excluded.

[Bryan Gin-ge Chen]

That may be true at the moment, but I don't think we want to keep people from using bold in docstrings for a reason like this. Also, from the doc-gen point of view, I think it'll be easier to work with a list of declarations that have been tagged by an attribute than trying to parse bold text out of docstrings.

[Yaël Dillies]

What about creating an attribute well_known "The name" which would allow to give statements/defs a name and would automatically index it on a dedicated webpage? To avoid manual interventions, it could classify the results automatically according to the folder structure.

[Bryan Gin-ge Chen]

It might be worth considering now whether we want more metadata attached to notable theorems than just a name. We could maybe follow the current tactic doc functionality and have a user command which allows us to also include URLs, DOIs, etc.

[Yaël Dillies]

Yes, that sounds like a great idea!

[Kevin Buzzard]

Stacks project tags...

[Bryan Gin-ge Chen]

I have a branch of doc-gen in progress locally which is supposed to consume URLs to the stacks project and put them on their own page. If there's a strong desire for it now I can move it up my Lean todo list, though we should probably discuss it back in this thread.

[Hunter Monroe]

For tagging definitions in mathlib, I prefer the bold () approach--it is user friendly to tag a definition for indexing with no new tags to learn, inline tagging avoids repeating the concept name, and doc_gen can easily extract what is between the ...** pair with a regular expression. URL/DOIs would be great not just for stacks but across multiple resources such as Wikipedia/MathWorld pages. I would like to see a free standing database of definitions/theorems that spans Lean, Isabelle, Coq, etc.

[Eric Wieser]

If we're looking at attribute-based tagging, perhaps overview.yml should be generated from attributes, which also has the advantage that moving a lemma doesn't break the yaml file

[Eric Wieser]

I guess the downside of that approach is that it's harder to bulk recategorize things

[Patrick Massot]

Hunter Monroe said:

Johan Commelin there is a need for a far more comprehensive auto-generated index of definitions and theorems covered in mathlib, with their conventional names not the mathlib names, than provided on the overview page, which would: (1) be more thorough, for instance, by including probability concepts (present in the undergrad page but not the overview page), and (2) by being thorough, would make it obvious from a glance what is not covered, for instance, random variables, expected value, central limit theorem). Mathlib has outgrown the manually maintained overview and undergrad pages. The documentation does not fill this need, for instance, see the search results for probability.

I'm not convinced at all, especially by the idea of collecting things based on visual markup (** tags). I think we're pretty far from having exhausted the capacity of manual overview pages. We simply need more PRs adding stuff to the overview.