Logo

Stream: general

[Yaël Dillies]

VSCode now lets extensions define icons for languages. Finally time for a proper .lean logo? :smiling_face:

[Jeremy Tan]

Yaël Dillies said:

VSCode now lets extensions define icons for languages. Finally time for a proper .lean logo? :smiling_face:

I always thought the current Lean logo was crappy, so (with my background in My Little Pony/furry vector art) I designed a new one
lean-logo.svg
lean-logo.png

[Jeremy Tan]

It's basically the "entails" symbol we always see in the Lean infoview, bisected in the horizontal arm to form an L and its mirror image Γ

[Jeremy Tan]

The logo can be exactly realised in pixel art as follows
image.png

[Yury G. Kudryashov]

Note that Lean is written as $\mathrm{L\exists\forall N}$ on the Zulip logo and in some other logo-like cases.