logo

Stream: general

[Jakob von Raumer]

The fact that another big theorem prover is having a discussion about logos reminde me of a little pet peeve of mine: There's always been a little step between the L and the E in Lean's logo (which hasn't changed since Soonho Kong created it in 2014). I edited the logo and created a PR for leanprover.github.io. Should I also apply the fix to other repos? /cc @Sebastian Ullrich @Patrick Massot

[Adam Topaz]

I never noticed this before, and, of course, now I can't unsee that little step...

[Kevin Buzzard]

I can't believe that nobody fixed the upside-down letters yet!

[Jakob von Raumer]

Adam Topaz said:

I never noticed this before, and, of course, now I can't unsee that little step...

That's why I haven't told anybody in years, I just wanted to spare you the pain ;)

[Jeremy Tan]

Kevin Buzzard said:

I can't believe that nobody fixed the upside-down letters yet!

:point_up:

[Yury G. Kudryashov]

I guess, this was a joke, because it's impossible to write it this way unless you do it on purpose.

[Asei Inoue]

@Jeremy Tan I love your logo!

[Kevin Buzzard]

If we're going to change the logo, maybe we should just rename the project Reanq? Edit: JOKE

[Martin Dvořák]

FYI, we have a #lean-logo channel on Discord:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Discord.20server.20Lean.204.20anarchy

PS: This kind of flame is exactly what I made the server for. Hence I suggest, guys, take it outside!

[Jeremy Tan]

Kevin Buzzard said:

If we're going to change the logo, maybe we should just rename the project Reanq?

Do I look like I even care about that? This is a serious point: Lean needs a universally recognisable logo like those of Python and Ruby if it is to reach its fullest potential. It can't just be an altered wordmark – it has to catch the eye.

And I intend to make my logo Lean's official one.

[Mauricio Collares]

Kevin replied with an even more obvious joke because you replied to his original joke as it if it were serious (and I'm only writing this message because the first part of your reply, which probably stems from missing the joke, is uncalled for in my opinion; the rest of the message is a valid point, even if I don't agree with it).

[Ruben Van de Velde]

To improve communication, we might end any message that's a joke with the tag "JOKE"

JOKE

[Kevin Buzzard]

Sorry for any confusion caused. It's a British convention that sometimes we communicate by saying the opposite of what we mean, and perhaps this does not come across well on the internet on a multicultural platform such as this one. Just to be clear: (1) I am aware that the letters in the current logo are upside down on purpose (2) I don't think we should change the name of the project (3) I don't think that one person suggesting that we change the logo of the project is a good reason to change the logo of the project, even if that person was extraordinarily helpful in the mathlib porting process and knows a lot about vector graphics.

[Kim Morrison]

Further, I would suggest that saying "I intend to make my logo Lean's official one." is not a productive way to try to initiate changes.

[Jeremy Tan]

Martin Dvořák said:

FYI, we have a #lean-logo channel on Discord:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Discord.20server.20Lean.204.20anarchy

PS: This kind of flame is exactly what I made the server for. Hence I suggest, guys, take it outside!

I had a look in that Discord server and found it inactive, so I guess my logo wasn't a flame at all

[Martin Dvořák]

Jeremy Tan said:

I had a look in that Discord server and found it inactive

You can post your logo there nevertheless. While it is very unlikely that your picture will become the official Lean logo, it can become the official "Lean 4 anarchy" logo!

[Ruben Van de Velde]

leanarchy

[Bulhwi Cha]

Bulhwi Cha said:

It's hard to see Lean's logo when using dark mode on a web browser or GitHub. A non-transparent image will solve the problem.

lean-firefox.png
lean-github.png

I just want the logo to be visible in dark mode.

[Junyan Xu]

That's called a "favicon" I think.

[Bulhwi Cha]

Do you mean the first one, not the second?

[Jon Eugster]

Would it be possible to detect dark mode and use the inverted favicon instead?

Something like

<link href="light-mode-favicon.png" rel="icon" media="(prefers-color-scheme: light)">
<link href="dark-mode-favicon.png" rel="icon" media="(prefers-color-scheme: dark)">

At least for me github's favicon is inverted when switching to dark mode. Not sure how they do it.

[Trebor Huang]

Another method is introducing a white boundary around the black part, which will work both without detection (in logos and avatars) and without introducing large patches of white (which defeats the purpose of dark mode)