Meet the community #

The Lean community is rather diverse. We have many users coming from mathematics, and some from computer science, and a few from other areas such as physics. Most users are students or academics, but there also some data scientists and software engineers working in industry.

Several teams of community members have designated responsibilities.

The map below can help you find members of the community geographically close to you.

If you want to add yourself to the above map, you can set the latitude and longitude fields in your Zulip profile; you can find your coordinates by right-clicking on the map. The map will be updated within 24 hours, the next time the website is built. We recommend indicating the coordinates of the main building where you work or study rather than the place where you live.

The Lean Zulip chat #

The main gathering point of our community is a Zulip chat instance. You can browse public discussions on the most popular “channels” without registering.

We welcome you to register for the Zulip chat, which will let you participate in the discussions. Registering with your real name is preferred, but not required. Starting by briefly introducing yourself in the new members channel is also appreciated.

Questions from users at all levels of expertise are welcomed. Asking your first questions in the new members channel will ensure the answers won't assume you know much about Lean. But you are welcome to use more specialized channels. Please start new discussion topics rather than using unrelated existing topics. If you need coding help, you may be asked to provide a "minimal working example" (MWE). Also beware of XY problems: try to give enough context.

To post a snippet of code inline, enclose it in single backticks: `my code here`. If your code contains backticks itself, enclose it in more backticks than it contains: `` my`code`contains`backticks ``.

Longer snippets should be enclosed between two lines containing three back-quotes, as in:

```
def n : myNat := 5
#check n
```

You can use LaTeX using $$ to enclose inline LaTeX and

```math
my LaTeX code here
```

for displayed math.

GitHub #

The next gathering point after Zulip is GitHub, which hosts all the community repositories. In particular, the mathlib pull requests page is the right place to see our ongoing efforts. You can also read about recent work on our blog.

There are many ways to contribute: developing new mathematical theories, adding to and writing documentation for existing theories, developing supporting software tools, and reviewing other people's proposed contributions. If you want to contribute to our projects then you can read our contributing guide.

Community guidelines #

We are devoted to developing an open and accepting community that welcomes participation from everyone. Behavior that is offensive, discriminatory, or aggressive will not be tolerated in any form. We adopt the Contributor Covenant Code of Conduct. These guidelines apply to the Lean Zulip chat and the leanprover-community GitHub organization.

The code of conduct team serves as first point of contact for reporting any concerns. We also provide an anonymous form to report incidents that violate the community guidelines.

We encourage a policy of de-escalation in the presence of unwelcome behavior. If you perceive someone acting in a way that violates our code of conduct, please do not respond in the same way; instead, take action to correct the behavior, such as reporting it to the moderators.