'theorem' or 'lemma'

Stream: mathlib4

[Peter Nelson]

Is there a mathlib style policy on this matter?

[Yaël Dillies]

Not yet, but the idea is to reserve theorem for named results in the mathematical literature, and call everything lemma

[Yaël Dillies]

Before enforcing this, we need to replace all mathport-induced theorem with lemma, and we're putting that off until we have a good programmatic solution

[Ruben Van de Velde]

Alternatively, we could just use one keyword and not have to argue which results should use which keywords

[Peter Nelson]

Based on those two responses, it seems that the intention might not be so clear-cut. Could some maintainers perhaps weigh in on this? When making PRs, it would be nice to have an official source indicating best practice, even if it's not enforced.

Note that it is difficult to search for an answer to this question on Zulip.

[Yury G. Kudryashov]

AFAIK, we don't have any official policy yet.

[Kyle Miller]

There's no official policy (and what Yaël says is an idea that has been suggested, though a reasonable one). My own preference is that theorem is reserved for what you feel is an important result in the theory. Almost all of mathlib consists of lemmas.

One of the things that didn't get ported when going from Lean 3 was which results were lemmas. I believe there's still some thought to try to port that eventually...

[Damiano Testa]

I have a script that replaces every theorem with lemma. I could adapt it to replace every "theorem with no doc string" to lemma. However, this rots very fast and I would only run it if it were certainly merged soon...

[Damiano Testa]

I could also write a linter that would enforce the "theorem must have a doc string".

[Kyle Miller]

It looks like we never made a decision, but I found the thread from September that was the last discussion about this, and somewhere in it was a poll that showed there was support to keep theorem for important results and to require that it have a docstring.

[Peter Nelson]

I like the sound of that enforced dosctring approach, or less stringently, the use of the keywords that aligns with the way mathematicians talk.

Sometimes though, as a contributor, it is just nice to be told what to do, and not to encounter differing views via PR suggestions (I'm not referring to anything specific recently, but I think I have had comments in the past suggesting lemma -> theorem for tiny results). Can I take it from this discussion that if I use 'lemma' and 'theorem' as if I were writing a paper, I won't meet any resistance?

[Ruben Van de Velde]

Not from me in any case :)

[Eric Wieser]

Note if you pick "theorem" but don't add a docstring, then it may be auto-replaced with lemma in future

[Damiano Testa]

I know that there are some strong views in favour and against the presence of lemma in mathlib. I am personally in favour.

In the meantime, I wrote a linter that warns against doc-less theorems in mathlib: #12869.

You can see its effect in #12863.

Note that the replacements theorem to lemma were guided by actually parsing the lean syntax. In particular, no doc-string or comment has been affected by the change.