Zulip Chat Archive

Stream: general

Topic: named theorems


view this post on Zulip Patrick Massot (Mar 12 2018 at 08:17):

We had endless conversation about lemmas which don't have names in maths and need a name in a proof assistant. But what about theorems that do have a name? Now in mathlib we have the squeeze theorem, that some mathematicians call the sandwich theorem and French mathematicians call the "théorème des gendarmes" (gendarme is a military version of policeman) but mathlib calls it: tendsto_of_tendsto_of_tendsto_of_le_of_le and we have Lagrange's theorem on the order of subgroups called in mathlib group_equiv_cosets_times_subgroup. Isn't it slightly problematic?

view this post on Zulip Patrick Massot (Mar 12 2018 at 08:17):

At least the squeeze theorem can be found by docstring grep

view this post on Zulip Simon Hudon (Mar 12 2018 at 08:25):

I always thought that those names made it harder to learn a subject. For instance, I came across Abelian groups multiple times not remembering what it was about while if it was referred to as a commutative group, I wouldn't even pause

view this post on Zulip Patrick Massot (Mar 12 2018 at 08:25):

Now I need to go to work (need do to stuff before that Gowers colloquium this afternoon)

view this post on Zulip Mario Carneiro (Mar 12 2018 at 08:28):

Personally, I prefer to relax the name-by-symbols approach for really famous or already named theorems. I would not have called it that tendsto tendsto tendsto thing, maybe some hybrid like tendsto_squeeze. For the second one, we could call it lagrange_theorem but the bigger issue is which of the possible slight variants on that theorem are to be the lagrange theorem

view this post on Zulip Mario Carneiro (Mar 12 2018 at 08:29):

I think I've mentioned this before, but I dislike theorems whose name has more than around 30 characters

view this post on Zulip Andrew Ashworth (Mar 12 2018 at 08:31):

i foresee for mathlib search by function name is going to become a big problem sooner rather than later

view this post on Zulip Mario Carneiro (Mar 12 2018 at 08:35):

To locate a result in mathlib, it is more effective to just go to the place where similar theorems are defined and look around. And topic organization is the relevant criterion for making this work, it is a much easier problem than good naming of all the theorems

view this post on Zulip Johannes Hölzl (Mar 12 2018 at 09:17):

I prefer to stay with the current system, as long as there is no proper search available. I also don't mind long theorem names as long as they are not used to often. For example the sandwich theorem is only used 15x in Isabelle's analysis. And usually at the beginning of a proof.

view this post on Zulip Mario Carneiro (Mar 12 2018 at 09:42):

Once you've disambiguated a theorem from all other theorems in the database, there's no further need to extend the name though. I honestly cannot imagine actually looking up the squeeze/sandwich theorem according to the symbols in its statement, especially since there is possible variation in that statement and a more high level description that indicates which variables are less than which is necessary for indicating the meaning anyway. In such a situation the conventional name is far more effective. (Plus, the whole reason for these naming conventions is because mathematicians never stepped up and named them themselves. When they do, I think it's better to defer to them.)

view this post on Zulip Kevin Buzzard (Mar 12 2018 at 10:01):

Maybe the simplest solution is just good docstrings, which mention all of the common names of a theorem. The fact that different cultures use the same ideas has always resulted in different naming conventions. I noticed when I lived in Paris that many results had some generic name in English but were called <French person>'s Theorem in French, for example (e.g. Bezout's Lemma, I had never heard it called that in the UK in the 90s).


Last updated: May 11 2021 at 21:10 UTC