Zulip Chat Archive
Stream: Zulip meta
Topic: The :lean: emoji
Anne Baanen (Apr 22 2021 at 19:53):
I have never dared to ask the story behind the 
emoji. Is this just an old version of the L∃∀N logo?
Mario Carneiro (Apr 22 2021 at 19:56):
No, it is independent, someone here on zulip made it to be a bit more colorful and square to work better as an icon
Mario Carneiro (Apr 22 2021 at 19:58):
Maybe someone else remembers who the author is
Anne Baanen (Apr 22 2021 at 20:00):
It says in the settings Rob added it as an emoji
Anne Baanen (Apr 22 2021 at 20:01):
Found it! It was @Bhavik Mehta's creation: https://leanprover.zulipchat.com/#narrow/stream/236604-Zulip-meta/topic/Logo/near/205365331
Kevin Buzzard (Apr 22 2021 at 20:09):
It's from the discord, there are a bunch of silly emojis there
Kevin Buzzard (Apr 22 2021 at 20:10):
Bhavik Mehta (Apr 22 2021 at 20:11):
None of these are silly!
Bhavik Mehta (Apr 22 2021 at 20:17):
except the emacs one
Anne Baanen (Apr 22 2021 at 20:18):
Well now I'm not going to add a VS code emoji :P
Last updated: Dec 20 2023 at 11:08 UTC