lemma

Stream: lean4

[Kenny Lau]

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

[Bryan Gin-ge Chen]

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

[Kenny Lau]

thanks!

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

can we have thm?

[Patrick Massot]

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

[Johan Commelin]

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

[Patrick Massot]

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...

[Johan Commelin]

that would make the meaningless choice a bit less meaningless

[Patrick Massot]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

Another example of meaningless syntax variation: variables vs. variable

[Mario Carneiro]

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

[Johan Commelin]

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 (-;

[Johan Commelin]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Mario Carneiro]

Okay, that's something

[Mario Carneiro]

Does most significant have a technical meaning?

[Patrick Massot]

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.

[Johan Commelin]

Mario Carneiro said:

Does most significant have a technical meaning?

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

[Johan Commelin]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

I myself am very conservative with using theorem

[Johan Commelin]

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) :

[Johan Commelin]

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...

[Johan Commelin]

but you get the point

[Mario Carneiro]

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

[Patrick Massot]

We'll handle that.

[Mario Carneiro]

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

[Mario Carneiro]

and don't say one of the 100 theorems

[Mario Carneiro]

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

[Mario Carneiro]

is the binomial theorem a theorem?

[Mario Carneiro]

additivity of integrals?

[Alex J. Best]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Kenny Lau]

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

[Johan Commelin]

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

[Kenny Lau]

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.

[Johan Commelin]

what does Stacks do?

[Kenny Lau]

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

[Johan Commelin]

~/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

[Kevin Buzzard]

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.

[Reid Barton]

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

[Kevin Buzzard]

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!)

[Filippo A. E. Nuccio]

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!

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

But how would we actually mark the distinction with comments?

[Reid Barton]

Isn't

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

strictly worse than

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

[Reid Barton]

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

[Julian Berman]

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

[Julian Berman]

(4% serious)

[Mario Carneiro]

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 : ...

[Kevin Buzzard]

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).

[Eric Wieser]

@[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.

[Simon Hudon]

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

[Joe Hendrix]

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

[Gabriel Ebner]

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