Is lean's logo here?

Stream: general

[crab]

image.png

is the lean logo here? i am wondering why it is absent, as this photo conatins logos of languages that are lesser known than lean

[Mario Carneiro]

No it's not. It wouldn't fit the color scheme :)

[Mario Carneiro]

as for why, you will have to ask whoever created that image

[crab]

the black and white logos
Mario Carneiro said:

No it's not. It wouldn't fit the color scheme :)

[Mario Carneiro]

Coq and Isabelle also aren't listed. Idris and F-star are the nearest thing I can see to theorem proving languages on the list

[crab]

Mario Carneiro said:

Coq and Isabelle also aren't listed. Idris and F-star are the nearest thing I can see to theorem proving languages on the list

coq is there

[crab]

as well as idris

[crab]

image.png

[Mario Carneiro]

Oh, there it is. Still, the point stands. It's a random image you found on the internet

[crab]

Mario Carneiro said:

Oh, there it is. Still, the point stands. It's a random image you found on the internet

with a lot of logos

[Mario Carneiro]

so it is

[crab]

and stupidly forgot to include lean

[crab]

[Mario Carneiro]

Actually, part of the issue might be that lean doesn't really have much of a logo

[crab]

L

[crab]

image.png

[crab]

image.png

[crab]

a logo

[Mario Carneiro]

there is a reason why both the logo in the top left and the emoji are not literally that logo

[Arthur Paulino]

Ah, marketing (getting widely known) is a completely different problem. I'd say don't worry about it for now

[Mario Carneiro]

but ultimately, you should direct your ire to the author of the image. People can make images with whatever they like

[Arthur Paulino]

For core devs, getting the thing to work is already hard enough. And for those of us who are still learning, it's also already hard enough

[crab]

why does lean not have a logo?

[Mario Carneiro]

because marketing is hard

[Arthur Paulino]

The process of making an appealing logo is a field of study in itself, we can't underestimate the effort needed for marketing

[crab]

lol

[Eric Wieser]

I know this has come up before, but who drew ?

[Mario Carneiro]

I think @Bhavik Mehta

[Jeremy Avigad]

Speaking of logos, I recently (politely) corrected yet another person who wrote LEAN instead of Lean, and they pointed out that it is probably the home page logo that leads people astray. A second explanation is that people may assume that it is an acronym. (Puzzle: what could it possibly stand for?)

[Arthur Paulino]

Interesting... having a logo that doesn't contain all the "Lean" letters would probably mitigate mistakes of that kind by unconsciously delivering the message that "this doesn't stand for the whole name, which is... let me check... Lean"

[Arthur Paulino]

having some fun with pixel art :rofl:
image.png

[Arthur Paulino]

Had this idea while doing dishes. If anyone wants to pick it up, vectorize, change it in any way, please feel free to. Or if any of the core devs wants to adopt it just let me know and I can polish it up

[Sebastian Ullrich]

Jeremy Avigad said:

Speaking of logos, I recently (politely) corrected yet another person who wrote LEAN instead of Lean, and they pointed out that it is probably the home page logo that leads people astray. A second explanation is that people may assume that it is an acronym. (Puzzle: what could it possibly stand for?)

We even have https://leanprover.github.io/lean4/doc/faq.html#is-it-lean-lean-or-ln (very bottom) now!

[Henrik Böving]

That's where I learned it from!

[Julian Berman]

Jeremy Avigad said:

(Puzzle: what could it possibly stand for?)

Highly productive Saturday morning activity.

Lemmas Easier Agreeably Named
Leave Everything admitted Needlessly
library_search Everything and Nap
Lean Embraces Axiomatic Nduction

[Henrik Böving]

I'm for the recursive one :p

[Jason Rute]

Logic Engine popularized by an Algebraic Number theorist

[Kevin Buzzard]

I laughed out loud at that one

[Kevin Buzzard]

More seriously, is it actually a fact that we do need some kind of logo which is not 1*4, as the current one is? Are logos typically more square? Does rust have a logo which fits nicely into a square? I know Coq and Isabelle do.

[Henrik Böving]

https://github.com/rust-lang/rust-artwork they have a bunch of logos for many form factors and uses.

[Henrik Böving]

Specifically https://github.com/rust-lang/rust-artwork/blob/master/logo/rust-logo-256x256.png (and related form factors) does fit into squares.

[Kevin Buzzard]

Do you think we need to talk to MSR about this? They might well want to design their own logos. I was lucky enough to talk to Leo recently and I know he has a lot of respect for Rust and how it has grown; I think he would love to see Lean taking a similar path.

[Arthur Paulino]

I'd be curious to see what they'd come up with. I was trying to come up with other ideas that would also represent the community in it

[Henrik Böving]

I would also expect that MSR either has people or contact to people that will be more capable of good design than we here.

[Arthur Paulino]

Ah, ofc. I was just trying to come up with ideas, not an actual final logo

[Arthur Paulino]

Where I work, the designers usually try to gather insights and ideas of any kind from those who use/develop the tools, so the design doesn't end up like a completely unrelated thing

[Stuart Presnell]

Does/should the mathlib project have a logo, distinct from that of the Lean language itself?

[Alex J. Best]

Whether or not the logo is different it would be really nice if the leanprover-community github account had an avatar that was recognizable and not the default github generated one, even @Johan Commelin's is more recognizable

[Yaël Dillies]

Yes, please!

[Julian Berman]

I wondered what made Johan the bastion of "even"s in that sentence, but after now seeing it, ok makes sense.

[Jeremy Avigad]

I once started making up a Lean logo that played on the famous sculpture (and US postage stamp):
https://en.wikipedia.org/wiki/Love_(image)
It's probably best left to someone with more artistic talent than me, and anyhow that pushes toward capital letters again.

It's funny, the community page has the word "Lean" 15 times in the main part and four more times in the sidebar, and still, somehow, people see "LEAN."

[Kyle Miller]

If the problem is that it's upper case, then lower case it is!

image.png

Upside-down lower-case ash is a lot funkier than I'd expected. Just to compare, upper case:

image.png

[Mario Carneiro]

I don't think flipping ae works since it's (approximately) invariant under the motion

[Rob Lewis]

@Edward Ayers made lots of logo suggestions a while back! image.png

[Julian Berman]

#dontopendeadinside

[Kyle Miller]

Lots of programming languages have cute mascots.

This, uh, isn't exactly one of those:

image.png

(I think this creature should never have escaped Inkscape, sorry.)

[Arthur Paulino]

A high contrast version of my previous idea:
image.png

[Patrick Massot]

I rather like this. Maybe it's a bit too tall.

[Eric Rodriguez]

Kyle Miller said:

Lots of programming languages have cute mascots.

This, uh, isn't exactly one of those:

image.png

(I think this creature should never have escaped Inkscape, sorry.)

lean + world of goo = this

[Rob Lewis]

To be serious for a second, I do think that proper branding/logo/etc for Lean is something MSR could deal with, probably supervised by the program manager they're looking to hire

[Rob Lewis]

And a mathlib/community logo could derive from this

[Rob Lewis]

Kyle Miller said:

image.png

But I'm fully in favor of Leanie as a community mascot

[Arthur Paulino]

Is it a fox? Looks like one :D

[Adam Topaz]

Arthur Paulino said:

Is it a fox? Looks like one :D

I'm pretty sure it's a play on :octopus: , which is more than appropriate!

[Yaël Dillies]

I actually hadn't noticed! It takes so much more sense now!

[Tomas Skrivan]

Where is the octopus actually coming from? There are bunch of octopuses when you search mathlib doc, was that just a random choice of emoji there?

[Kevin Buzzard]

I think the octopus is a Zulip thing. It's always there amongst the "popular emojis" in the PC app

[Kalle Kytölä]

I'm sure the cute :octopus: would popularize quantifier yoga!

[Junyan Xu]

https://glif.app/@Junyan/runs/clmrhiz680052l60g1et5izg8
https://glif.app/@Junyan/runs/clmrhks8c007kl70fiwj6zhfa
image.png
image.png

Where's the :tada:? :eyes:

[John Baker]

How about this?

new_lean_logo.png
new_lean_logo.tex

[Newell Jensen]

(deleted)

[Newell Jensen]

Or this? Nod to @John Baker for what he had.

lean-logo.png

[Mario Carneiro]

I'm not sure people will even be able to read that if they don't already know what it's supposed to say

[Matthew Pocock]

The green one, but without the i? Perhaps make the lambda a little more bold, so that it has similar visual weight to the N. Also, nudge it it to the right a bit to equalize the dead space against the E with the dead space the E has with the A.

[Scott Morrison]

We're not changing the logo. :-)

[Junyan Xu]

image.png
“a bunch of mathematicians typing on laptops with blackboards in the background”
https://glif.app/glifs/clmqp99820001jn0f2xywz250
Hmm I don't think we usually wear suits like this ...

[Patrick Massot]

I don't think this kind of post is relevant here.

[Newell Jensen]

@Patrick Massot if you look closer they are spelling out Lean

[Newell Jensen]

That is probably why @Junyan Xu posted it

[Patrick Massot]

I still don't think this is relevant.

[Junyan Xu]

I think this thread is about designing logos or producing other forms of art (mascots etc.) that helps creating and popularizing Lean's image in the broader public. However, the latest post was in early 2022, before AI art became popular. I want to inform artists here of the new possibilities opened up by novel AI techniques based on ControlNet that can embed messages into pictures in a natural way. The method has recently become popular through scannable QR codes, Spiral Town, and most recently embedded text and logos, and there are now several online services that allow you to generate images using a prompt (general description of the image) and the text you want to embed, such as the one I use.

[Scott Morrison]

Yes, I think this thread would be better suited e.g. for discord.

[Scott Morrison]

If that's not suitable, we could start a "tea" stream, for relaxed off-topic discussion.

[Scott Morrison]

That would need a moderator who would plausibly ensure participants still follow the code of conduct.

[Mario Carneiro]

I'd rather we not have a "tea" stream at all. For stuff that trends slightly off topic it's fine to keep them in their respective streams, and for stuff that goes farther I think we should just not have it on the zulip. I very much like the high signal to noise ratio of the zulip and think such a stream would add more noise.

[Bhavik Mehta]

What about having a "tea" stream which is opt-in, so the majority of users maintain the current signal-to-noise ratio, but those interested can subscribe to a more relaxed stream (and voluntarily increase the noise they receive). Though, as Scott says, this would require moderation.

[Martin Dvořák]

What about publicly displaying a link to one of the above-mentioned Discord servers?

[Bolton Bailey]

Lean has a Discord?

[Yaël Dillies]

Xena Discord server, held by Kevin, to discuss his formalisations of his mathematics in his theorem prover, Lean.

[Martin Dvořák]

Bolton Bailey said:

Lean has a Discord?

That's exactly the point. People keep telling us "keep that crap to Discord; it doesn't belong here" but then they don't give us a link to the Discord server.

[Bolton Bailey]

Yaël Dillies said:

Xena Discord server, held by Kevin, to discuss his formalisations of his mathematics in his theorem prover, Lean.

Ah ok yes. That's meant for undergrads, if I recall, so I have not joined it.

[Martin Dvořák]

I was (al least once) told there is also another Discord server for Lean users, not only for mathematicians, but I don't know what it is or how to get there.

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20lean.20discord.20server

[Martin Dvořák]

Xena Discord is private, I get it.
Is the other one public?

[Mario Carneiro]

it seems to be dead now

[Martin Dvořák]

Maybe it wouldn't be dead if people knew how to join it.

[Mario Carneiro]

or at least the invite link is, dunno if anyone got in and knows how to share a link

[Bhavik Mehta]

I might be misremembering, but I recall joining it, and I believe the creator of that deactivated their zulip and discord accounts and closed down the server

[Martin Dvořák]

OK, then I'll create one.