Lean Trademark Policy

Not Appearing Official, Affiliated, or Endorsed

The most basic rule is that the Lean Trademarks cannot be used in ways that appear (to a casual observer) official, affiliated, or endorsed by Lean FRO, unless you have written permission from Lean FRO. This is the fundamental way we protect users and developers from confusion. This is a requirement for all uses, even those that are listed as not requiring explicit approval. For example, the use of terms such as ‘official’, ‘original’ or ‘only’, (e.g. ‘The official Lean Reference’), is likely to give the appearance that the use of the trademark is officially endorsed by Lean FRO, and therefore would not be acceptable.

Since this rule is about managing perception, it is subjective and somewhat difficult to nail down concretely. If you have any doubts, we would be more than happy to help.

The Basics: Referring to Lean

As with any trademark, the Lean name (and the stylized version of the Lean name) can be used with minimal restriction to refer to the Lean programming language and theorem prover.

Always use any trademark as an adjective only, followed by a generic noun. For instance, it is correct to refer to the Lean programming language and theorem prover (adjective) but not simply to Lean (noun). Don't use the trademark as a verb ("Lean your software today!"). Also acceptable is the Lean programming language (adjective) and the Lean theorem prover (adjective).

Logos must be used in the form provided by Lean FRO, and must be accompanied by a symbol for unregistered trademarks: "(TM)" or a small "™". This may not be removed or obscured and must always be included with the logo.

The Lean Trademarks may not be used:

• To refer to any other programming language or theorem prover;

• To refer to a modified version of the Lean programming language and theorem prover, except as permitted below for minor changes;

• In a way that is misleading or may imply association of unrelated modules, tools, documentation, or other resources with the Lean programming language and theorem prover;

• In ways that confuses the community as to whether the Lean programming language and theorem prover is open source and free to use.

Legitimate Sources of Official Source Code of the Lean Programming Language and Theorem Prover and Associated Binaries

Official source code and binaries produced by Lean FRO will always come from one of these sources; however, not everything on these domains is official or covered by this policy.

• The domain lean-lang.org and its subdomains

• The Github Organisation “leanprover” (located at https://www.github.com/leanprover) and its projects

Uses That Do Not Require Explicit Approval

There are a variety of uses that do not require explicit approval. However, in all of the cases outlined below, you must ensure that use of the Lean Trademarks does not appear official, affiliated or endorsed, and always as an adjective, as explained above.

The following uses do not require explicit approval:

• Stating accurately that software is written in the Lean programming language and theorem prover, that it is compatible with the Lean programming language and theorem prover, or that it contains code written in the Lean programming language and theorem prover, is allowed. In those cases, you may use the Lean name, or stylized name, to indicate this, without prior approval. This is true both for non-commercial and commercial uses.

• Using the name Lean, or stylized name, in the name of packages or code repositories in e.g. GitHub, is allowed when referring to use with or compatibility with the Lean programming language and theorem prover.

• Using the Lean name, or stylized name, in publicly distributed, modified versions of the Lean programming language and theorem prover is allowed, provided that the modifications are limited to:

  • Code adjustments for the purpose of porting to a different platform, architecture, or system, or integrating the software with the packaging system of that platform.

  • Hosting a fork of the code for the purpose of making changes, additions, or deletions that will be submitted as contributions to the official Lean programming language and theorem prover code repositories is allowed, as long as you do not market or promote your fork.

• Using the Lean Trademarks on t-shirts, hats, and other artwork or merchandise is allowed for your personal use or for use by a small group of community members, as long as they are not sold.

• Using the Lean Trademarks for social and non-profit events like meetups, tutorials, and the like is allowed for events that are free to attend. Your materials for the event must not imply that the event is officially endorsed or run by Lean FRO unless you have written permission. For commercial events (including sponsored ones), please check in with us.

• Using the Lean Trademarks on websites, brochures, documentation, academic papers, books, and product packaging to refer to the Lean programming language and theorem prover is allowed.

Uses That Require Explicit Approval

Distributing a modified version of the Lean programming language and theorem prover is permitted under the terms of the Apache 2.0 license. Distributing a modified version of the Lean programming language and theorem prover with modifications other than those permitted above and calling it Lean, or otherwise identifying it through use of Lean Trademarks requires explicit, written permission from Lean FRO. We may allow these uses as long as the modifications are (1) relatively small and (2) very clearly communicated to end-users. We encourage research projects that explore changes to Lean, and will take the needs of distribution for research purposes into account when asked for permission to distribute.

The following uses require explicit approval from Lean FRO:

• Selling t-shirts, hats, and other artwork or merchandise including the Lean Trademarks requires explicit, written permission from Lean FRO. We will usually allow these uses as long as (1) it is clearly communicated that the merchandise is not in any way an official product of Lean FRO and (2) it is clearly communicated whether or not profits benefit Lean FRO.

• Using the Lean Trademarks within another trademark requires written permission from Lean FRO and may include additional conditions of use and a fee for use.

• Using the Lean Trademarks in connection with commercial or large non-profit events (including industry and academic conferences) requires explicit, written permission from Lean FRO. We will usually allow these uses, though conditions of use may be applied on a case-by-case basis.

• Creating a derived logo from the Lean Trademarks always requires permission. We will usually not allow this in order to avoid placing a confusing logo into wide-spread use.

We reserve the right to request proofs prior to production in any situation that requires explicit approval of use.

If you don’t see your situation covered by these guidelines, please get in touch and we’ll be happy to help!