Stream: lean4

Topic: lemma

Kenny Lau (Jan 05 2021 at 21:44):

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

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

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.

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

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!

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

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

Mario Carneiro (Jan 06 2021 at 15:45):

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

Reid Barton (Jan 06 2021 at 16:12):

But how would we actually mark the distinction with comments?

Reid Barton (Jan 06 2021 at 16:12):

Isn't

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


strictly worse than

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


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

Julian Berman (Jan 06 2021 at 18:09):

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

(4% serious)

Mario Carneiro (Jan 06 2021 at 18:21):

Reid Barton said:

But how would we actually mark the distinction with comments?

/-- The binomial theorem -/

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

@[simp] lemma smul_zero : ...


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

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.

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

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

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