Lean is programming language which allows one to turn mathematical proofs into a type of program. The important things to note before we get into design are two unicode symbols: ∀ and ∃. ∀ means “for all” and ∃ means “there exists”, so for instance, ∀x ∃y x < y says “for all numbers x there exists a number y such that y is greater than x”. These are rather fundamental symbols in mathematical proofs and thus deserve the place they have in Lean’s logo. Now to the logo:
something’s wrong, I can feel it
I hope I’m not alone in thinking that this is… just off somehow. I think I can easily isolate a few things I don’t like: the L running into the ∃ is very awkward and I don’t like it, and the ∀ feels boxed in next to the ∃ and the N. These can be fixed with a very simple fix: just space out the letters a bit:
Maybe it’s just me, but this doesn’t feel quite fixed? I suppose it’s helpful now to lay out the things I like about the design: I like the extremely thin lettering, and feel like it gives a light, well… lean feel to the logo. I think what I don’t like is how the math symbols don’t feel properly separate from the Latin characters, and as a result the whole thing feels like it’s about to flip over clockwise. I first made the simplest possible fix:
I’m not always this lazy I swear
I think this is a major improvement from the original. I messed around a bit making the math symbols in a slightly different font or making them heavier/thicker, but haven’t yet found a good balance. What do you think?