Is the Lean Logo "Open Source"?

Stream: general

[Pedro Abreu]

Hi all! :wave:

I'm the host of the Type Theory Forall podcast and website (https://typetheoryforall.com), where I explore topics in type theory, PL, and formal methods through longform interviews and accessible content.

I recently started a small merch shop to help support the project and have begun selling mugs featuring the Rocq logo (with their blessing). I'd love to do something similar with the Lean logo—just a simple mug design with the logo on it.

Before moving forward, I wanted to ask: is the Lean logo considered open source, or otherwise freely reusable for something like this? If there are any guidelines or restrictions I should follow, I'd be happy to comply.

Thanks in advance!

—Pedro

[Johan Commelin]

I've passed your question on to the Lean FRO.

[Pedro Abreu]

much appreciated!

[James E Hanson]

The Lean logo is part of the Lean FRO's trademark filing, if that means anything.

[(deleted)]

Correct, and trademark is the only thing that matters here. The logo doesn't pass the threshold of originality, so it's ineligible for copyright.

[Mario Carneiro]

and usage of the lean logo to refer to lean would of course be in keeping with the lean trademark