lemma vs theorem

Stream: mathlib4

[Eric Wieser]

Patrick Massot said:

Honestly that lemma vs theorem information is not worth fighting for. Our current mathlib [edit: 3] is a mess here.

Now that we're in a position where mathport has replaced every lemma with theorem; should we just remove the lemma keyword?

[Johan Commelin]

Seems like there are > 5000 lemmas in ml4 already

[Eric Wieser]

Then I would guess the distinction is ported vs new-in-mathlib4.

[Eric Wieser]

Or maybe ported-without-mathport

[Notification Bot]

4 messages were moved here from #mathlib4 > Mario's FMM 2021 talk by Eric Wieser.

[Eric Wieser]

Johan Commelin said:

Seems like there are > 5000 lemmas in ml4 already

A regex for (^|\] )lemma only finds ~1300 matches for me

[Eric Wieser]

Eric Wieser said:

Then I would guess the distinction is ported vs new-in-mathlib4.

This is of course evidence that no one likes typing theorem and everyone prefers the shorter lemma; but having both seems pointless if the distinction is really mathport output vs not

[Yaël Dillies]

Then maybe we should abolish theorem in mathlib?

[Eric Wieser]

I'd be happy with that (and a lint rule banning theorem) too; I just think it's noise to have both now that all the deliberate uses have been completely eliminated by the port

[Martin Dvořák]

I always decide between writing lemma and theorem deliberately. Am I the only one who cares?

[Martin Dvořák]

Eric Wieser said:

Now that we're in a position where mathport has replaced every lemma with theorem

I think it is technically possible to write a script that will change theorem to lemma for all theorems that resulted from porting a lemma from Mathlib 3.

[Eric Wieser]

I think it is technically possible to write a script that ...

Sure, but we already made the decision not to care about this when we started the port (see the message I quoted at the top of the thread, and what it's in reply to)

[Martin Dvořák]

Ah, sorry. Did you mean that Mathlib 3 was a mess in this regards?

[Eric Wieser]

Yes, Patrick's comment was referring to mathlib 3, edited to make that clear.

[Kyle Miller]

I try to use lemma vs theorem meaningfully.

I think Patrick's comment was that it's not worth going through the engineering effort to get Lean 3 to give mathport lemma vs theorem information. That doesn't mean that we wouldn't want to be able to choose whether a result is a lemma or a theorem.

[Kyle Miller]

Eric Wieser said:

This is of course evidence that no one likes typing theorem and everyone prefers the shorter lemma

You should consider the fact that most results in mathlib are individually fairly trivial lemmas, so it shouldn't be surprising that you'd find more lemmas than theorems

[Eric Wieser]

If that's the case, maybe a good compromise is to globally replace every theorem that is #aligned (i.e., from mathport) with lemma?

[Kyle Miller]

This is fun, apparently "theorem", if you follow the etymology, could be replaced with "behold!"

[Jon Eugster]

If the current state is such a mess I'd even consider just replacing every theorem with lemma in all of mathlib and then only mark hand selected ones back as theorems over time as they come up. That way it would be clear that everything marked as theorem is intentional

[Eric Wieser]

Yes, I think that's what I intended to suggest above

[Damiano Testa]

If using lemma is forced by linting, then calling something a theorem would involve also using a nolint. This would likely mean that simply grepping for the nolint would give a curated list of results which I would definitely consider a plus!

[Eric Wieser]

Perhaps a rule should be that theorems require docstrings? (but of course lemmas are allowed them too)

[Johan Commelin]

I like that!

[Johan Commelin]

And also a reference to external literature

[Damiano Testa]

That works also, although it makes grepping trickier.

The reason for wanting a grep-friendly solution is mostly due to the current increasing interest in mathlib: it might be helpful to be able to extract what are the "main" results also for someone who know almost nothing of lean...

[Johan Commelin]

We can lift that rule by the time people do original maths research directly in mathlib PRs

[Johan Commelin]

@Damiano Testa Why is it hard to grep for theorem?

[Damiano Testa]

It is not hard to grep for theorem, but it is not easy to only receive information that is not in a doc-string.

[Damiano Testa]

Anyway, the grep issue is just a side concern. Requiring doc-strings and a possible reference is already great!

[Jon Eugster]

Lean is inheritally not grep friendly though, I think you're much better off improving the available lean tooling that yields that information (like Kyle demonstrated recently) or improve the #docs so that you can easily filter for theorems.

[Damiano Testa]

Sure, although I have the impression that I am not the only one who finds that getting a rough estimate using grep is much quicker than learning how to meta-program it exactly.

[Kyle Miller]

Is that convenience worth making all contributors need to add a greppable @[nolint]?

I think it would be less effort overall to get the mathlib docs to have generated theorem indexes. The point isn't that you'd be expected to write these metaprograms personally, but rather that someone could improve the tooling to generate this sort of thing.

[Damiano Testa]

Sure, I am not trying to argue that grep is the ultimate goal. However, here is a case that I have had in my mind and have not had the strength to meta-program: what is the ratio between auto-generated/actually human-typed declarations?

I can get the exact count of declarations from Kyle's earlier metaprogram. After that, I still find it easier to grep for lines that roughly begin with "lemma" or "theorem" and accept a possible miscount to get an estimate.

I am not sure how to go about meta-programming an actual correct count, though...

[Eric Wieser]

Perhaps Kyle's metaprogram should be committed to mathlib in a scripts/ or examples/ directory

[Damiano Testa]

Eric: definitely. I saved it already!

[Mario Carneiro]

I agree with Damiano's point that having both lemma and theorem makes grepping harder. Even if we have fancy metaprogramming search mechanisms (and we don't currently), these would still require compiling mathlib to get accurate information. Grep works without any infrastructure, and can work on github code search too

[Kevin Buzzard]

lemma is not a core Lean keyword, it's introduced in mathlib as a synonym for theorem on the basis that mathematicians like to distinguish between trivialities and interesting stuff rather than calling everything a theorem (which is a bit grandiose)

[Jireh Loreaux]

But this is now totally out of whack because mathport translated everything as theorem.

[Eric Wieser]

I think we're waiting for someone to reset everything by doing a global replacement

[Damiano Testa]

Should the reset call every theorem lemma or actually match what was used in Lean 3?

[Eric Wieser]

I think just do a full reset

[Damiano Testa]

I like the challenge! Let me give it a try!

[Eric Wieser]

We could follow up by converting anything that contains something like **the Pythagorean theorem** etc back to a theorem

[Kevin Buzzard]

For years there was some comment in core Lean containing a word with a random alpha in instead of an a, because of a global rename fail; I look forward to the fun that this idea will bring :-)

[Damiano Testa]

Well, you can see the progress: #7079!

The current version is building on my computer and reached approximately 1k files with no errors.

I may have inadvertently changed a theorem to a lemma in a doc-string. If this is an issue, I can be more careful!

[Damiano Testa]

By the way, when CI was building mathlib, it would show how many files it build and how many were missing. This seems to be gone, or am I missing something?

[Eric Wieser]

You can only see this on GitHub if you keep the page open

[Eric Wieser]

In progress logs from before you opened the page are not shown

[Damiano Testa]

I caught a few more replacements: there are currently almost 100k changed lines, and I think that there are about 100k (explicit) lemmas in mathlib, right? So, this is looking superficially reasonable! :upside_down:

[Kevin Buzzard]

I tried to find some errors but your method had dealt with them all correctly.

[Kevin Buzzard]

If we're interested in this, it should probably be merged the moment it compiles.

[Damiano Testa]

If it builds, I think that the only errors would be doc-strings where a theorem has been replaced by a lemma: not a ideal, but probably not too problematic either... we'll see! :smile:

[Damiano Testa]

since the process is essentially automatic, if the doc-string replacements is an issue, I can make sure that doc-string theorems are unchanged.

[Sebastien Gouezel]

Can't this be done by metaprogramming (i.e., Lean itself), to be sure that everything is right? @Mario Carneiro

[Damiano Testa]

I think that it should be possible, but for me it was easier to do the bulk replacement in bash.

[Damiano Testa]

Also, the consequences of an error are probably not too big: at worst, something that was theorem has been replaced by lemma. :smile:

[Damiano Testa]

CI uploaded the cache! But then failed on Archive. I'll take a look!

[Damiano Testa]

Turns out that huang_degree_theorem had become huang_degree_lemma!

[Joachim Breitner]

I guess you are lucky that lemma is shorter than theorem, else you’d have to deal with the :100: :capital_letters: :stop_sign:

[Damiano Testa]

Yes, I thought of that!

The PR is linting: all the building of mathlib, archive, tests, counterexamples is done!

[Damiano Testa]

It's green!

[Mario Carneiro]

Sebastien Gouezel said:

Can't this be done by metaprogramming (i.e., Lean itself), to be sure that everything is right? Mario Carneiro

Yes, this would be covered under my plans for bulk syntax edits (although I haven't actually moved on that plan)

[Utensil Song]

(EDIT: message moved back to https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/List.20of.20important.20keywords/near/391609134 )

[Damiano Testa]

Mario Carneiro said:

Sebastien Gouezel said:

Can't this be done by metaprogramming (i.e., Lean itself), to be sure that everything is right? Mario Carneiro

Yes, this would be covered under my plans for bulk syntax edits (although I haven't actually moved on that plan)

A first conflict appeared in the PR. Mario, does your comment mean that this change should wait? If so, great and I will close the PR! Otherwise, I'll keep it afloat for a while! Note that it is not much work, since the changes are essentially automatic.

[Mario Carneiro]

I think it is best to just wait until we are basically already about to hit the merge button since this PR conflicts with everything and will be disruptive to existing PRs as well

[Mario Carneiro]

Note that this is going to be one more thing where Std diverges from Mathlib because Std only uses theorem while mathlib now only uses lemma

[Mario Carneiro]

In many other programming language ecosystems there are concerns about "splitting the ecosystem" or "creating a dialect" and FYI this is exactly what mathlib is doing

[Damiano Testa]

I completely agree with your points and I rationally understand.

However, at a less rational level, I found that looking at the pages and pages of lemmas was very welcoming! I feel that if the convention had been "you can only use lemma", I would not have thought "oh, we really need theorems"!

Anyway, I will not maintain the PR, but the conversion theorem to lemma is automatic, so it can be reproduced on-demand!

[Eric Wieser]

Mario Carneiro said:

In many other programming language ecosystems there are concerns about "splitting the ecosystem" or "creating a dialect" and FYI this is exactly what mathlib is doing

Mathlib4 has already done this by defining the lemma command in the first place. Either we should define it and use it for the majority of mathlib, or we should remove it.

[Damiano Testa]

Also, as far as dialects go, in the context of formalizing mathematics, being allowed to use either lemma or theorem seems pretty innocuous and I doubt that it will be the hardest thing you come by, learning Lean. :upside_down:

[Mario Carneiro]

Eric Wieser said:

Mario Carneiro said:

In many other programming language ecosystems there are concerns about "splitting the ecosystem" or "creating a dialect" and FYI this is exactly what mathlib is doing

Mathlib4 has already done this by defining the lemma command in the first place. Either we should define it and use it for the majority of mathlib, or we should remove it.

Or we should upstream it

[Mario Carneiro]

Damiano Testa said:

Also, as far as dialects go, in the context of formalizing mathematics, being allowed to use either lemma or theorem seems pretty innocuous and I doubt that it will be the hardest thing you come by, learning Lean. :upside_down:

It's more problematic than you might think, because when people learn about how def and theorem have a bunch of subtle differences even though you can use def for theorems and theorem for defs, they might logically expect that there is also some subtle difference between lemma and theorem, but no this is only a style difference (except that if you copy and paste a lemma into std it won't parse)

[Mario Carneiro]

I don't like keywords that have no meaning. It should do something, for example appearing higher on the docs page or being a different color or hiding access from other files etc. This keyword is currently just completely useless and misleading

[Mario Carneiro]

Currently there isn't even a way to differentiate theorems from lemmas after the fact if you wanted to show a list of theorems somewhere

[Mario Carneiro]

and I would argue the nonexistence of such tooling directly correlates with how low quality the actual signal is, no one will upkeep this thing if it doesn't do anything

[Damiano Testa]

I remember someone had suggested that theorems should require a doc-string, while lemmas need not have one. I think that this is very much in line with how I feel about the meaning of those words. Would this be something that (maybe in the future) would help?

[Damiano Testa]

I realize that this is just a style issue, but at least there is something that you can say that distinguishes the two, besides the characters that you need to type!

[Mario Carneiro]

lemma is 2% less likely to trigger the line length lint :)

[Damiano Testa]

That settles it, then! :rofl:

[Alex J. Best]

I'm not sure I'm convinced by this PR, seeing as at the moment there is no difference between theorem and lemma (other than length. I wonder if the extra macro expansion is noticeable in !bench though). And one downside is it pollutes the git history, I often use git blame to see why a certain thing is set up that way or find the PR that introduced / changed it, now I'll have to click through some steps to find that information for every theorem lemma line in mathlib

[Mario Carneiro]

I agree that this is a "formatting" PR and should probably be bundled with other "format the world" style PRs to minimize disruption

[Eric Rodriguez]

the history is completely broken already unless Eric (other) has done the history rewriting yet

[Eric Wieser]

It's on my todo list, competing with actually writing the rest of my thesis...

[Eric Wieser]

I don't think the history pollution is too bad here; we can always add it to the list of commits to exclude from git blame(.git-blame-ignore-revs)

[Alex J. Best]

Eric Rodriguez said:

the history is completely broken already unless Eric (other) has done the history rewriting yet

Well a lot of what I've worked on recently could be classed as cleaning up from the port so I'm actually quite interested in seeing the discussion during the port mostly. But I didn't know about git-blame-ignore-revs which settles my concern completely

[Alex J. Best]

It looks like the name of that file and usage is simply a convention though that everyone would have to set up as a git config themselves, but its better than nothing

[Mario Carneiro]

the usage in github is not a convention

[Alex J. Best]

Well what I mean is that git itself will not if I do git blame in the command line or in the editor without extra configuration. Github already does it which is good yes.

[Eric Wieser]

The extra config is blame.ignorerevsfile=.git-blame-ignore-revs (via git config)

[Eric Wieser]

Then it appears everywhere

[Patrick Massot]

Mario Carneiro said:

In many other programming language ecosystems there are concerns about "splitting the ecosystem" or "creating a dialect" and FYI this is exactly what mathlib is doing

I'm much less worried that lemma is creating a dialect than the mathlib option of removing autoImplict is creating a dialect. It's really annoying that I can't copy-paste Lean code from the Lean 4 stream into my Mathlib scratch file. To be clear, lemma is adding something to Lean. It is no surprise that Mathlib has more things than core Lean. The idea to remove features from Lean in Mathlib is much more disturbing and unexpected.

[Mario Carneiro]

Note that I said std, not core lean. I would really like the divergence between std and mathlib to be primarily about library additions rather than language additions (which should ideally be achieved by upstreaming mathlib utility commands and tactics to std), but std is stylistically more similar to core than mathlib and doesn't set any options (except for linter.missingDocs, because docs are important)

[Kevin Buzzard]

The fact that removing autoImplicit has broken Std has completely changed my opinion on the matter. autoImplicit was annoying during the port, but Std now being broken is just as annoying.

[Eric Wieser]

I'm hoping that problem will end up irrelevant due to the lake changes Mario is proposing. I assume you're not also advocating that the non-strict autoimplicits (all identifiers permit typos) are restored to mathlib?

[Eric Wieser]

Because that setting also breaks (much less) of Std

[Patrick Massot]

Strict autoImplicits seemed like a really good compromise.

[Jireh Loreaux]

Unfortunately (IMO) the poll didn't really agree: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib4.3A.20autoImplicit.20false.20by.20default.3F/near/384265143

[Mario Carneiro]

TBH that poll seems pretty split

[Patrick Massot]

And that poll took place before people could see how annoying is the ban on autoImplicit.

[Jireh Loreaux]

(I won't fight revisiting it!)

[Eric Wieser]

Patrick Massot said:

And that poll took place before people could see how annoying is the ban on autoImplicit.

Arguably what we're seeing is how annoying lean4#2455 is; I don't think we should re-vote unless we're giving up on lean4#2456

[Mario Carneiro]

I think you mean lean4#2455

[Mario Carneiro]

(I'm sure lean4#2555 will also be annoying)

[Notification Bot]

67 messages were moved here from #new members > List of important keywords by Eric Wieser.

[Eric Wieser]

Mario Carneiro said:

I don't like keywords that have no meaning. It should do something, for example appearing higher on the docs page or being a different color or hiding access from other files etc. This keyword is currently just completely useless and misleading

Mario Carneiro said:

and I would argue the nonexistence of such tooling directly correlates with how low quality the actual signal is, no one will upkeep this thing if it doesn't do anything

In light of these, I would really like it if we could remove one of lemma or theorem from mathlib. It's annoying to see a PR of the form

lemma foo1 : sorry := sorry
lemma foo2 : sorry := sorry
lemma foo3 : sorry := sorry
theorem bar1 : sorry := sorry
theorem bar2 : sorry := sorry
theorem bar3 : sorry := sorry
lemma baz1 : sorry := sorry
lemma baz2 : sorry := sorry
lemma baz3 : sorry := sorry

where the only signal here is either "bar was moved from another file but baz/foo are new lemmas" or "I am sending an SOS message via steganography".

[Yaël Dillies]

As we discussed somewhere else, can we force theorems to have a docstring? And if they don't have one, give a warning "theorem is reserved to important (named) results, and therefore should be explained by a docstring. For lesser results, use lemma.".

[Kevin Buzzard]

I don't like keywords that have no meaning. It should do something, for example appearing higher on the docs page or being a different color or hiding access from other files etc. This keyword is currently just completely useless and misleading

0 is equally useless and misleading, right? It's just another name for Zero.zero, but with fewer characters.

[Eric Wieser]

In that situation though:

• We effectively have a rule of "never write Zero.zero"
• It is not possible to eliminate Zero.zero from existence leaving only 0

[Eric Rodriguez]

Yaël Dillies said:

As we discussed somewhere else, can we force theorems to have a docstring? And if they don't have one, give a warning "theorem is reserved to important (named) results, and therefore should be explained by a docstring. For lesser results, use lemma.".

wouldn't we want to advocate for both theorem/lemma to be core Lean in that case?

[Eric Rodriguez]

Eric Wieser said:

In that situation though:

• We effectively have a rule of "never write Zero.zero"
• It is not possible to eliminate Zero.zero from existence leaving only 0

crazy, but why not replace Zero.zero with OfNat 0?

[Eric Wieser]

You mean OfNat Zero.zero?

[Eric Wieser]

I think the main answer to "why not use OfNat 0?" is "it would have been really annoying during the port"

[Eric Wieser]

Revisiting that is probably a question for a separate thread though.

[Mario Carneiro]

Eric Rodriguez said:

crazy, but why not replace Zero.zero with OfNat 0?

We definitely tried that, it didn't work

[Mario Carneiro]

the problem is that you can't have a class that extends OfNat A 0, OfNat A 1

[Yaël Dillies]

Eric Rodriguez said:

Yaël Dillies said:

As we discussed somewhere else, can we force theorems to have a docstring? And if they don't have one, give a warning "theorem is reserved to important (named) results, and therefore should be explained by a docstring. For lesser results, use lemma.".

wouldn't we want to advocate for both theorem/lemma to be core Lean in that case?

We can just override the theorem macro mathlib-wise.

[Eric Wieser]

I'm not sure what value "theorem must have docstrings, lemma doesn't need to" provides that "use theorem everywhere, put docstrings on important results" doesn't

[Yaël Dillies]

We can have them tagged with a theorem attribute and collect them (or at least their number) on some webpage?

[Yaël Dillies]

I think that would be interesting for cross-library comparisons because mathlib has an order of magnitude more lemmas than eg Isabelle.

[Scott Morrison]

Probably this is obvious from my previously expressed biases, but I would love to simply remove lemma. It it noise, and as Mario says introduces a split in the ecosystem for apparently very little gain.

[Matthew Pocock]

It is confusing as a noob that people (and some docs/tooling?) talk about lemmas but the only thing that exists in the language is theorem. If we think in terms of an API, my intuition is that the theorems are the public-facing API, and the lemmas are the extra things that needed to be implemented to make that work, or to make it work more nicely. I agree with people who are saying that if both lemma and theorem are to co-exist, that there should be some language-level difference between them, or else the distinction may as well be by convention or an attribute or something.

[Johan Commelin]

My preference:

• keep both, for socialogical reasons
• if we really need to sacrifice one of them, then please remove theorem. Upgrading every stupid lemma to a theorem could very well be seen as pretentious. But downgrading every famous theorem to a lemma might lead to a nice chuckle in the audience.

[Kevin Buzzard]

The issue for mathematicians is that a + c = b + c -> a = b really is not a theorem to them, it is a triviality and we have a good name for these. From Wikipedia: "Generally, an assertion that is explicitly called a theorem is a proved result that is not an immediate consequence of other known theorems. Moreover, many authors qualify as theorems only the most important results, and use the terms lemma, proposition and corollary for less important theorems. "

I am very unclear about how to weight this sociological issue against the objection from the CS side about dialects of the language, an objection which to me sounds frivolous but it's being made by people I trust.

[Eric Wieser]

Upgrading every stupid lemma to a theorem could very well be seen as pretentious.

The thing is, we already did this when porting, and no one seems to have complained. The documentation labels every stupid lemma as a theorem anyway.

[Johan Commelin]

Nobody in our community complained. Because we wanted to get the port done.

[Eric Wieser]

The lean 3 documentation also never showed the difference between lemma and theorem

[Eric Wieser]

I'd claim that people outside our community would look at the docs not the code

[Bolton Bailey]

I think people would understand that this is a programming language which has chosen the keyword theorem to represent "A proposition which has been proven true", and that to a computer without the aesthetics and deep understanding of a human, there is no difference between a theorem and a lemma.

[Johan Commelin]

Whenever I'm looking at Lean stuff with an experienced mathematician who doesn't know Lean, I apologize when we see a theorem blah_blah_triviality ...

[Kevin Buzzard]

...and the explanation is what Bolton just posted.

[Johan Commelin]

There was a time when mathlib called every field/topological space/group/metric space/ring/vector space/etc alpha, or when that was taken it used beta.

[Johan Commelin]

We stopped doing that, for pretty similar reasons.

[Bolton Bailey]

To be clear, I also think it would be fine to keep using both. It's not like we're talking about just using def for everything, even though that's semantically equivalent too.

[Eric Wieser]

I see no point using both if the choice between them is random, as it currently is for the majority of statements. We still have to explain to mathematicians why we wrote theorem, but the answer is the less satisfying "oh, it's just a mess that is too big to clean up"

[Eric Wieser]

Or if we decide we're going to reset to lemma everywhere in mathlib (which I think is better than doing nothing), and start marking significant results, then the explanation for theorem my_trivial_result becomes "oh, that lemma comes from core/Std and <Bolton's explanation>"

[Yaël Dillies]

Hopefully, mathematicians will encounter lemmas from Core/Std less often.

[Yaël Dillies]

Further, in the case we implement my suggestion (override mathlib-wise theorem to be a macro tagging the declaration with a @[theorem] attribute, and then use that attribute to display declarations as either theorem or lemma in the docs), then theorems from Core/Std will actually not have been tagged with @[theorem] and therefore appear as lemmas in the mathlib docs.

[Eric Wieser]

So lemma means theorem and theorem means @[theorem] theorem?

[Johan Commelin]

Eric Wieser said:

"oh, it's just a mess that is too big to clean up"

We're proud of our bold refactors of the library. I think we can clean up this mess.

[Damiano Testa]

I think that part of the issue is also that there is no such clear distinction between theorem, lemma, corollary, proposition in maths. There are some results that to most "feel" like theorems, others that are lemmas and so on, but others are murky, I would say.

[Yaël Dillies]

Eric Wieser said:

So lemma means theorem and theorem means @[theorem] theorem?

Precisely.

[Eric Wieser]

Damiano Testa said:

I think that part of the issue is also that there is no such clear distinction between theorem, lemma, corollary, proposition in maths. There are some results that to most "feel" like theorems, others that are lemmas and so on, but others are murky, I would say.

I think this is particularly true for things like associativity on elliptic curves; I assume this would be considered a theorem, but because add_assoc is stated super generally it's just a lemma

[Damiano Testa]

But the murkiness does not justify, in my opinion, eradicating the possibility of expressing oneself! :smile:

[Damiano Testa]

Eric Wieser said:

Damiano Testa said:

I think that part of the issue is also that there is no such clear distinction between theorem, lemma, corollary, proposition in maths. There are some results that to most "feel" like theorems, others that are lemmas and so on, but others are murky, I would say.

I think this is particularly true for things like associativity on elliptic curves; I assume this would be considered a theorem, but because add_assoc is stated super generally it's just a lemma

Sure, in this case, I would say that the theorem is that an elliptic curve is a projective group-scheme.

[Damiano Testa]

add_assoc on an elliptic curve is a lemma, a very useful one!

[Eric Wieser]

What happens if a mathematician considers powerful_result a theorem, but in mathlib we prove it as a special case like even_more_powerful_result 0; is powerful_result a theorem or a lemma?

[Damiano Testa]

Eric, I think that these are edge-cases and we may choose a convention for how to reproduce, within mathlib, exact results in the literature. I still welcome to option to have a discussion about it, though!

[Eric Wieser]

Damiano Testa said:

But the murkiness does not justify, in my opinion, eradicating the possibility of expressing oneself! :smile:

If we leave the possibility in, we now have to review code from newcomers who pick randomly between theorem and lemma; which means we need to write down rules for reviewing whether things are a theorem or a lemma, and reviewers have to apply these rules.

[Johan Commelin]

Eric Wieser said:

What happens if a mathematician considers powerful_result a theorem, but in mathlib we prove it as a special case like even_more_powerful_result 0; is powerful_result a theorem or a lemma?

corollary :stuck_out_tongue_wink:

[Johan Commelin]

Eric Wieser said:

If we leave the possibility in, we now have to review code from newcomers who pick randomly between theorem and lemma; which means we need to write down rules for reviewing whether things are a theorem or a lemma, and reviewers have to apply these rules.

If theorem requires a docstring, then they will very quickly learn to use lemma almost always.

[Eric Wieser]

I would guess the result would actually be lots of useless docstrings, especially as the lean manual is going to have pushed theorem quite heavily.

[Eric Wieser]

Of course those are easy to catch in review, but a waste of everyone's time!

[Yaël Dillies]

Eric, do you really think this will happen if we implement the following suggestion of mine as well?
Yaël Dillies said:

As we discussed somewhere else, can we force theorems to have a docstring? And if they don't have one, give a warning "theorem is reserved to important (named) results, and therefore should be explained by a docstring. For lesser results, use lemma.".

[Johan Commelin]

Nah, if the linter tells you to use lemma or write a docstring, I'm sure most people will choose the easy option

[Yaël Dillies]

People are lazy, Eric, and we can leverage it. :wink:

[Eric Wieser]

/poll What should we do?

• Replace all theorems with lemmas and introduce a stricter theorem as described
• Replace all lemmas with theorem and eliminate lemma from mathlib
• Do nothing, the status quo is fine

[Jireh Loreaux]

I'm really torn on this issue. As a mathematician, the choice in my mind is trivial: use both and make theorem require a docstring and use it for named/important theorems (corollary and other alternatives I think are not necessary). However, I also feel a very strong pull to avoid deviating from the rest of the Lean ecosystem; I think there is value in cohesiveness. On the other hand, maybe we'd be setting a precedent.

[Eric Wieser]

We could remain consistent with Std if we had theorem/real_theorem instead of lemma/theorem, but I doubt anyone wants that!

[Alex J. Best]

I think cohesiveness is nice, but there are already many many other reasons why code from mathlib cannot always be copy-pasted into Std so I don't really see a difference between this situation and irreducible_def for example. If lemma was roughly just a macro for @[lemma] theorem and we had a linter for docstrings on all theorems that don't have that attribute, then we wouldn't be overriding the theorem keyword in any way, simply adding an extension.

[Alex J. Best]

(it would be very nice to have a tool that automatically elaborates all steps (or maybe just the macros) defined in a subset of imported files (but no others) and prints the result, which could be used as a de-mathlibifier, I've no idea how feasible that is in practice though)

[Bolton Bailey]

Johan Commelin said:

corollary :stuck_out_tongue_wink:

Coq apparently also has Remark, Fact, Corollary, Proposition

[Kevin Buzzard]

I think one issue about allowing multiple names for the same thing is that one person's theorem is another person's lemma. Although mathematically I'm slightly uncomfortable, I'm going to follow Scott and Mario and vote for killing lemma, because they seem to think that this is important, and at the end of the day I don't think I really care. The fact that Mario is so vehemently anti two names for the same thing is in particular something which worries me.

[Antoine Chambert-Loir]

Kevin Buzzard said:

The issue for mathematicians is that a + c = b + c -> a = b really is not a theorem to them, it is a triviality

And as all trivialities, it is quite false as quoted…

[Kevin Buzzard]

Well, there are of course some obvious assumptions which I omitted :-)

[Damiano Testa]

For a trivial theorem with fewer assumptions, we can also consider a = a.

[Jireh Loreaux]

But docs#rfl is a def (!!) :laughing:

[Jireh Loreaux]

Apparently the truly important theorems get upgraded to that status. :stuck_out_tongue_wink:

[Matthew Pocock]

Johan Commelin said:

Nah, if the linter tells you to use lemma or write a docstring, I'm sure most people will choose the easy option

Particularly if the linter disallows empty or trivial docstrings, and if the IDE has a code refactoring action to "fix" the undocumented theorem as a lemma.

[Matthew Pocock]

The Rust tooling is excellent IMHO at integrating the compiler and linting errors and warnings with suggestions and IDE actions to address them. They seem to have a policy that the tooling never tells you anything is wrong without giving you an explanation for why and also at least one suggested fix. In my experience >90% of the time the suggestion is correct.

[Matthew Ballard]

I can imagine a mathematician being pretty salty when their theorem is declared a lemma by leanprover-community.

[Ruben Van de Velde]

I think the best argument for only having the one keyword is not having to argue about which one to use

[Frédéric Dupuis]

Indeed, I'm not looking forward to having to bring this up when reviewing PRs.

[Eric Wieser]

Frédéric Dupuis said:

Indeed, I'm not looking forward to having to bring this up when reviewing PRs.

That's why whatever decision we make, it should be enforced by CI as much as possible; it's much more pleasant for both parties dealing with a picky linter than a picky reviewer, even if they say the same thing!

[Mario Carneiro]

Bolton Bailey said:

Johan Commelin said:

corollary :stuck_out_tongue_wink:

Coq apparently also has Remark, Fact, Corollary, Proposition

By the way, lean used to as well, it originally got them from Coq. I don't think it had all of these but corollary existed in lean 2 IIRC. Lean has scaled back on synonymous theorem-introducers since then