Zulip Chat Archive

Stream: new members

Topic: the expression 'Lean'

Claus-Peter Becke (Sep 16 2020 at 08:16):

Obviously 'Lean' is a special type of acronym. The second and the third letter are written as quantifiers. Thus the acronym is composed of symbols which refer Lean to logical issues. But what stand the first and the fourth letter for? 'n' for numbers? 'L' for logic?

Johan Commelin (Sep 16 2020 at 08:24):

I wouldn't be surprised if you are looking for something that doesn't exist... (but I might be wrong)

Kenny Lau (Sep 16 2020 at 08:25):

I think it's just the "lean" in boolean

Anne Baanen (Sep 16 2020 at 08:26):

The abbreviation of "Boolean" is also the story I was told. It's also one of 4 completely gender-neutral names in the Netherlands (i.e. in the most recent data I could find, from 2007, it was registered as the first name of 46 men and of 46 women).

Patrick Massot (Sep 16 2020 at 08:29):

You're all wrong.

Patrick Massot (Sep 16 2020 at 08:30):

I found it! https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Teaching.20lean.20to.20high.20school.20students/near/132137220

Kenny Lau (Sep 16 2020 at 08:32):

so why is it called Lean

Alex Peattie (Sep 16 2020 at 08:44):

I chose the name "Lean" because I wanted it to be smaller and simpler than Z3

I think it's using the meaning of lean as an adjective, as in a "lean organization" :smile:

Patrick Massot (Sep 16 2020 at 08:44):

Because Z3 is fat

Patrick Massot (Sep 16 2020 at 08:45):

Or, more precisely, Lean is leaner than Z3.

Patrick Massot (Sep 16 2020 at 08:47):

I think you're meant to see something like http://tpeabkr.e-monsite.com/medias/album/sprinter-marathonien.jpg

Patrick Massot (Sep 16 2020 at 08:48):

So that it doesn't sound too negative for Z3.

Claus-Peter Becke (Sep 16 2020 at 09:11):

Thank you very much for your helpful explanations.

Last updated: Dec 20 2023 at 11:08 UTC