Zulip Chat Archive

Stream: general

Topic: official name for lean user

Matthew Ballard (Aug 04 2022 at 18:12):

Is there an official name for a lean user?

Jireh Loreaux (Aug 04 2022 at 18:24):

Is this a thing? I mean, is there an official name for a python user? Sorry if it sounds snarky, not intended as such.

Matthew Ballard (Aug 04 2022 at 18:28):

Pythonista I believe

Mauricio Collares (Aug 04 2022 at 18:28):

That was Pythonista some time ago (see, e.g., https://david.goodger.org/projects/pycon/2007/idiomatic/handout.html), not sure if it's still used

Matthew Ballard (Aug 04 2022 at 18:29):

I was hoping for a poll...

Adam Topaz (Aug 04 2022 at 18:39):

Let's try to avoid "luser" ;)

Matthew Ballard (Aug 04 2022 at 18:41):

Too much work to add the L-hand sign over the forehead.

Jireh Loreaux (Aug 04 2022 at 18:48):

Interesting, I had no idea.

Matthew Ballard (Aug 04 2022 at 18:48):

"Unclean" is probably not great either

Matthew Ballard (Aug 04 2022 at 18:52):

/poll For fun, what is your preferred name for a Lean user

leaner
leanagander
leanian
cerulean
herculean

Yaël Dillies (Aug 04 2022 at 19:13):

Tom Forster is calling the Cambridge Lean students "leanies".

Yaël Dillies (Aug 04 2022 at 19:14):

Also, Bhavik and I are currently resisting the urge to rename the Cambridge Lean group "CLean".

Adam Topaz (Aug 04 2022 at 19:21):

Just don't start a rivalry with the oleans from Oxford ;)

Eric Rodriguez (Aug 04 2022 at 19:27):

maybe that's where we need to look for algebra/order/field :)

Kalle Kytölä (Aug 04 2022 at 19:33):

On the important ~~off~~topic of local Lean clubs... Ours is ForAlli (= formalization alliance). Our logo is naturally:
foralli.png

I'm particularly proud :upside_down: of how we successfully avoided any resemblance with our university's logo:
Aalto-logo-73049-1.png

Arthur Paulino (Aug 04 2022 at 19:39):

"Leanie" sounds really good for a mascot name. I recall Kyle's amazing drawing :joy_cat:

Kalle Kytölä (Aug 04 2022 at 19:42):

Here's that amazing drawing, in case someone missed it.

Matthew Ballard (Aug 04 2022 at 19:50):

This is a plushie version of John Carpenter's The Thing. (I mean this in the most complementary way.)

David Renshaw (Aug 04 2022 at 20:43):

some suggestions from a large language model: "Leanhorn", "Leandroid"

David Renshaw (Aug 05 2022 at 17:19):

Leanderthal, Leanbag, Leanographer, Leanologist, Leanguist, Leanaut, Leanid, Oleander, Leanut, Sophoclean, Leangineer, Soylean, Galilean, Leanto, Leaning, ...

Matthew Ballard (Aug 05 2022 at 17:24):

Leanderthal is quite evocative

David Renshaw (Aug 05 2022 at 17:32):

Leanbacker, Leansman, Trampolean, Pralean, Adrenolean, ...

Asei Inoue (Feb 24 2025 at 06:18):

Python users are sometimes called "Pythonistas," so I thought "Lean player" would be a good-sounding nickname for Lean users. What do you think?

Reasons for promoting this nickname:

"Lean Prover" and "Lean Player" have similar pronunciations.
Lean provides a game-like UI for mathematics, so its users might be called "players."

Rado Kirov (Feb 24 2025 at 06:26):

I mean Leaninists is really on the tip of my tongue. I think Pythonistas is also a play on a political movement (Sandinistas?), might be too much though.