Zulip Chat Archive

Stream: lean4

Topic: lemma


view this post on Zulip Kenny Lau (Jan 05 2021 at 21:44):

How do I make a macro to let lemma mean theorem?

view this post on Zulip Bryan Gin-ge Chen (Jan 05 2021 at 22:07):

A slight modification of the defthunk example from the "Beyond Notations" paper:

macro "lemma" id:ident ":" type:term ":=" proof:term : command =>
`(theorem $id : $type := $proof)

lemma blah : True := trivial

view this post on Zulip Kenny Lau (Jan 05 2021 at 22:08):

thanks!

view this post on Zulip Johan Commelin (Jan 06 2021 at 05:41):

so now we can have conjecture foo : bar quux and it means theorem foo : bar quux := sorry (-;

view this post on Zulip Mario Carneiro (Jan 06 2021 at 09:41):

Can we maybe take the opportunity to banish lemma in lean 4? This is a meaningless choice that is confusing in light of all the other choices that are not meaningless

view this post on Zulip Johan Commelin (Jan 06 2021 at 09:43):

can we have thm?

view this post on Zulip Patrick Massot (Jan 06 2021 at 09:43):

Calling everything a theorem sounds more ridiculous to me than calling everything a lemma.

view this post on Zulip Johan Commelin (Jan 06 2021 at 09:44):

we could have a linter that requires that theorem has a docstring

view this post on Zulip Patrick Massot (Jan 06 2021 at 09:44):

I noticed that, among the many influence of Lean on my real world mathematics practice and especially teaching, I've started to call almost everything lemma in my teaching...

view this post on Zulip Johan Commelin (Jan 06 2021 at 09:44):

that would make the meaningless choice a bit less meaningless

view this post on Zulip Patrick Massot (Jan 06 2021 at 09:45):

Note how great it is that Leo doesn't need to care about this discussion! If I understand correctly we can add or remove such commands in mathlib at any time.

view this post on Zulip Mario Carneiro (Jan 06 2021 at 09:57):

I actually banished lemma in an early commit in mathlib (it was like commit number 4) but it didn't make it into the style guide and ultimately didn't stick

view this post on Zulip Mario Carneiro (Jan 06 2021 at 09:58):

I think that using a smaller lexicon for what to call "true/proven things" is just a good idea, I don't personally care what word we use but I think "theorem" is the technically/logically correct one

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:00):

There are lots of other ways in which mathematical lexicon is boiled down to simpler terms to get encoded in lean. I'm not sure why this is a point of contention

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:02):

Another example of meaningless syntax variation: variables vs. variable

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:03):

Having more keywords is generally a bad thing, unless the new keywords have new meanings

view this post on Zulip Johan Commelin (Jan 06 2021 at 10:03):

I agree with you on variable/variables. But there is too much emotional baggage in the theorem vs lemma distinction. I wouldn't pick that battle (-;

view this post on Zulip Johan Commelin (Jan 06 2021 at 10:03):

Mario Carneiro said:

Having more keywords is generally a bad thing, unless the new keywords have new meanings

Right, so I propose to make docstrings required for theorems

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:03):

But to this day I don't think we have a clear style guide on what to call a theorem in mathlib

view this post on Zulip Patrick Massot (Jan 06 2021 at 10:04):

It's not only about emotion, it's also about navigating the library. We need some way to quickly highlight the most significant results.

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:04):

Okay, that's something

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:04):

Does most significant have a technical meaning?

view this post on Zulip Patrick Massot (Jan 06 2021 at 10:04):

Mario Carneiro said:

But to this day I don't think we have a clear style guide on what to call a theorem in mathlib

That's mainly because at some point during prehistory, someone decided to call everything a theorem and it messed up everything.

view this post on Zulip Johan Commelin (Jan 06 2021 at 10:05):

Mario Carneiro said:

Does most significant have a technical meaning?

nope, it's historical/psychological, as far as I can see.

view this post on Zulip Johan Commelin (Jan 06 2021 at 10:05):

But it's the stuff that is considered a milestone, that get's mentioned in the module docs, and that deserves a decent docstring

view this post on Zulip Patrick Massot (Jan 06 2021 at 10:05):

This discussion reminds me of the dark ages when every type was named by a Greek letter.

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:05):

The thing is, even when we have "named" theorems we often have several variations, it's not a 1-1 match with literature anyway

view this post on Zulip Bryan Gin-ge Chen (Jan 06 2021 at 10:06):

So you're saying we need to add corollary as well... :joy:

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:07):

There are some theorems that are clearly Theorems, some things that are simp lemmas, and MANY things in between

view this post on Zulip Johan Commelin (Jan 06 2021 at 10:08):

right... but many parts of the style guide leave room for flexibility

view this post on Zulip Johan Commelin (Jan 06 2021 at 10:08):

I myself am very conservative with using theorem

view this post on Zulip Johan Commelin (Jan 06 2021 at 10:08):

rg "theorem" src/ring_theory/witt_vector/*.lean
src/ring_theory/witt_vector/structure_polynomial.lean
16:In this file we prove the main theorem that makes the whole theory of Witt vectors work.
126:theorem witt_structure_rat_prop (Φ : mv_polynomial idx ) (n : ) :
136:theorem witt_structure_rat_exists_unique (Φ : mv_polynomial idx ) :
288:theorem witt_structure_int_prop (Φ : mv_polynomial idx ) (n) :
315:theorem witt_structure_int_exists_unique (Φ : mv_polynomial idx ) :
320:theorem witt_structure_prop (Φ : mv_polynomial idx ) (n) :

view this post on Zulip Johan Commelin (Jan 06 2021 at 10:09):

that's all the theorems in Witt vector stuff. Of course the "theorem" that Witt (zmod p) is Z_p is actually a def, etc...

view this post on Zulip Johan Commelin (Jan 06 2021 at 10:09):

but you get the point

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:09):

I just don't want to have to think about this distinction

view this post on Zulip Patrick Massot (Jan 06 2021 at 10:10):

We'll handle that.

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:11):

Is there any theorem in list.basic? finset.basic? bigops? Where are theorems?

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:12):

and don't say one of the 100 theorems

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:12):

I mean in the day to day theorems, what constitutes a theorem?

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:13):

is the binomial theorem a theorem?

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:14):

additivity of integrals?

view this post on Zulip Alex J. Best (Jan 06 2021 at 10:14):

Its completely subjective of course, but people here are just saying that despite it being an imperfect measure they still prefer to have some demarcation of say 5% (also a subjective number) of results in mathlib that are most mathematically interesting.

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:14):

I would still like to have some criterion that we can put in the style guide

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:15):

is it theorems that are referred to externally? Theorems with documentation seems like a good idea but it doesn't sound like a sufficient condition

view this post on Zulip Mario Carneiro (Jan 06 2021 at 10:16):

I just have no conception of what this metric is at all

view this post on Zulip Patrick Massot (Jan 06 2021 at 10:19):

That's not a problem Mario. Don't worry, we'll handle this.

view this post on Zulip Kenny Lau (Jan 06 2021 at 10:22):

Euclid uses Πόρισμα (corollary) <29 times, Λῆμμα (lemma) <26 times, and all the propositions in his book are just numbered but are referred to as θεώρημα (theorem)

view this post on Zulip Johan Commelin (Jan 06 2021 at 10:38):

@Kenny Lau I'm sure you know of the great vowel shift...

view this post on Zulip Kenny Lau (Jan 06 2021 at 10:39):

I guess what I said is just meant to be some sort of weak connection to the past. Maybe we should look up some famous math paper written in the 21st century then.

view this post on Zulip Johan Commelin (Jan 06 2021 at 10:42):

what does Stacks do?

view this post on Zulip Kenny Lau (Jan 06 2021 at 10:50):

Lemma: < 53260 times
Remark: < 3051 times
Theorem: < 2001 times
Proposition: < 1976 times
Corollary: 0 times

view this post on Zulip Johan Commelin (Jan 06 2021 at 10:52):

~/tmp/stacks-project$ for t in lemma proposition theorem proof example exercise equation history reference remark remarks situation; do echo -en "$t\t"; rg begin\\\{$t | wc -l; done
lemma 11743
proposition 303
theorem 206
proof 12296
example 420
exercise 366
equation 667
history 3
reference 242
remark 937
remarks 5
situation 116

view this post on Zulip Kevin Buzzard (Jan 06 2021 at 11:41):

Mario Carneiro said:

I just have no conception of what this metric is at all

It is a judgement which is partly aesthetic and partly pragmatic -- stuff which is either important or beautiful or in some sense the "main result in the area" might be called a theorem. There is a difference in meaning, but it is not something which one can quantify. The fundamental theorem of Galois theory is a theorem because it's what you just spent 3 lectures proving technical lemmas working up to. You then never apply the technical lemmas again but you use the theorem all the time. It's perhaps something to do with results which guide the human learner. Lean does not need to know the distinction but it is an important organisational principle for humans. You don't get an overview of a maths topic by being told 100 true Props but you do get one if you're told the key definitions and the key theorems, of which there will be far fewer.

view this post on Zulip Reid Barton (Jan 06 2021 at 11:45):

Bourbaki has probably > 50% Propositions, and the rest Theorems, Corollaries, and a few Lemmas which are even typeset a bit differently.

view this post on Zulip Kevin Buzzard (Jan 06 2021 at 11:56):

Yes, Proposition is somewhere between a lemma and a theorem, but apparently the CS people use it to mean something else :-/ (they can have false ones! Can you believe it!)

view this post on Zulip Filippo A. E. Nuccio (Jan 06 2021 at 14:14):

Although irrelevant, I can't resist quoting the (very much cited) snake Lemma (nobody would call it the snake Theorem) or Shapiro's Lemma. My favorite one is yet the "Ugly Lemma" by Tate (and/or Serre) in Cassels&Frohlich, whose adjective was, I guess, meant to make it forgotten resulting in it being unforgettable. Then there is the fundamental Fundamental Lemma... What a nightmare!

view this post on Zulip Mario Carneiro (Jan 06 2021 at 15:40):

Of course I know that there are dozens of different names mathematicians use for proved things. But I'm not convinced that this is a distinction which is meaningful in a formal development outside of comments. It quite clearly has all the mess of natural language in it, just like the difference between properties that are adjectives vs properties that are nouns

view this post on Zulip Mario Carneiro (Jan 06 2021 at 15:43):

Kevin Buzzard said:

Yes, Proposition is somewhere between a lemma and a theorem, but apparently the CS people use it to mean something else :-/ (they can have false ones! Can you believe it!)

"the CS people" -> philosophers, but I guess this works in the definition of CS = everything other than mathematics

view this post on Zulip Mario Carneiro (Jan 06 2021 at 15:45):

and logicians (which are again not mathematicians under kevin's worldview)

view this post on Zulip Reid Barton (Jan 06 2021 at 16:12):

But how would we actually mark the distinction with comments?

view this post on Zulip Reid Barton (Jan 06 2021 at 16:12):

Isn't

/- lemma -/ lemma foo : ...
/- theorem -/ lemma bar : ...

strictly worse than

lemma foo : ...
theorem bar : ...

view this post on Zulip Reid Barton (Jan 06 2021 at 16:47):

I fully grant that, in agreement with Wadler's Law, this discussion is about the lexical syntax of comments

view this post on Zulip Julian Berman (Jan 06 2021 at 18:09):

obviously the solution is instead lemma foo : and lemma bar_theorem :

view this post on Zulip Julian Berman (Jan 06 2021 at 18:09):

(4% serious)

view this post on Zulip Mario Carneiro (Jan 06 2021 at 18:21):

Reid Barton said:

But how would we actually mark the distinction with comments?

/-- The binomial theorem -/
lemma add_pow_eq_sum : ...

/-- The fundamental lemma -/
lemma fundamental_lemma : ...

@[simp] lemma smul_zero : ...

view this post on Zulip Kevin Buzzard (Jan 06 2021 at 18:40):

The fundamental lemma is a historical artefact. The Langlands poeple thought it would be a combinatorial triviality in the 70s but it turned out to be extremely deep (Ngô Bảo Châu got a Fields Medal for proving it).

view this post on Zulip Eric Wieser (Jan 06 2021 at 20:51):

@[significant] would be an alternative to a keyword or comments. Whatever the choice, I can only see it being useful if we also train doc-gen to show these theorems specially.

view this post on Zulip Simon Hudon (Jan 06 2021 at 21:02):

I added an attribute that I called main_declaration already so that I can detect the dead code in a file. I think that's very closely related

view this post on Zulip Joe Hendrix (Jan 06 2021 at 22:37):

These distinctions might help with code navigation as well. I could see, for example, configuring the VSCode outline to show "theorems" but not "lemmas".

view this post on Zulip Gabriel Ebner (Jan 29 2021 at 10:19):

For anybody else who didn't notice it: the lemma keyword is gone from Lean 4 core.


Last updated: May 18 2021 at 22:15 UTC