I completely agree. Lemmas are simple, obvious, and yet they completely change how you think.

How many proofs cite the Axiom of Choice? How many cite Zorn's Lemma? Which is more important, the axiom that we're relying on, or the restatement of the axiom that allows us to actually prove things?

It is not just mathematics that values simple and obvious ideas that change how you think. We all should value that. Like Stein's Law, "Things that can't go on forever, don't." And Davies' Corollary, "Things that can't go on forever, can go on longer than you think they can."

• signa11

  today at 8:51 AM

  > Lemmas are simple, obvious, and yet they completely change how you think.

  speak only for yourself :o) , they are the reason we have:

      lemma now, dilemma later

  • ForceBru

    today at 9:08 AM

    Yeah, I can't say lemmas are (generally, or even often) simple and obvious. To me, they often seem arbitrary: what do you mean before we prove this grand theorem we have to prove these completely unrelated lemmas? Okay, proved the lemmas. Now the proof of the theorem has "according to such and such lemmas..." sprinkled around, but I've already forgotten what the lemmas were and why they're applicable. I also can't name any lemmas that changed how I think.

• emil-lp

  today at 6:40 AM

  I'm not sure your choice is the best. Axiom of choice is an axiom, not a theorem. In addition, axiom of choice is frequently stated (contrary to most other axioms) in proofs and assumptions.

Favorite lemmata:

Johnson–Lindenstrauss lemma

https://en.wikipedia.org/wiki/Johnson%E2%80%93Lindenstrauss_...

Isolation lemma

https://en.wikipedia.org/wiki/Isolation_lemma

Schwartz–Zippel lemma

https://en.wikipedia.org/wiki/Schwartz%E2%80%93Zippel_lemma

Lovász local lemma

https://en.wikipedia.org/wiki/Lov%C3%A1sz_local_lemma

• dchftcs

  today at 9:05 AM

  The division of lemmas and theorems is really a bit artificial for these things. But yeah I think the spirit is that a theorem is an object that you aim to study, while a lemma is something you use to do that. Fermat's last theorem was a target, but the techniques including lemmas used and developed for it are the real prize for a working mathematician. Sculptures are kind of the point, but there's no question the tools used for sculpting are more useful and "worth" more in that sense.

> Even more important than lemmas are observations, but that is another story.

In my book about abstraction logic (http://abstractionlogic.com) I have definitions, theorems, lemmas, and even observations :-) Just did a count of the frequency. Of course, not sure what those frequencies say about the relative importance.

-----------

Definitions 78

Theorems 20

Lemmas 76

Observations 41

I guess homological algebra must be worth at least a million theorems, then?

coyoneda lemma has been helping me out (in prod - at FAANG even!) for over a decade

• LPisGood

  today at 3:02 AM

  How has it helped in production software? Are you writing a lot of Haskell?

  • whateveracct

    today at 5:43 AM

    yes

(2007)

[dead]