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.

To clarify the above: actions that can result in suspension or banning from the Lean community Zulip include harassment, discriminatory or disrespectful behavior, sustained off-topic or disruptive posts, repeated low effort posts, use of the community to complete coursework or work tasks, use of sock-puppet accounts, DM spam, unsolicited mass DMs to users, significant use of AI without attribution, unrequested posting of "slop" AI-generated code, making unjustified and incorrect claims about AI-generated code, and ignoring moderator guidance.

This is not a free code review service. Posts that amount to 'look at my project' without a specific question or prior community involvement will be removed and the poster suspended.

Please do not use an LLM when writing comments on github or Zulip. Don't worry if English is not your native language: this is true for most users; as long as you can be understood, you will be fine. Building community involves human connection; using an LLM to write for you removes this human element. Messages and comments that appear LLM-generated will be deleted, and can lead to suspension.

This list is not exhaustive and the maintainers retain broad discretion in user moderation.

Repeated violations will result in temporary suspensions, which will increase in length if the behavior continues. Egregious individual incidents will result in bans.

The code of conduct team serves as first point of contact for reporting any concerns. You can write to members of this team directly or use an anonymous form to report incidents that violate the community guidelines. Specifically on Zulip, you can also report problematic messages to the whole moderation team (made of Mathlib and CSLib maintainers and some Lean FRO members), see the relevant Zulip documentation. Only the moderators can see that you reported a message, and what you wrote in your report.

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.

Purview of the Moderation and Code of Conduct teams #

This section serves to distinguish the purposes and roles of the Code of Conduct and Moderator teams. In addition, this will serve to clarify some of responsibilities of those roles, and as such, is a public-facing document.

The Lean Zulip has nearly 16,000 subscribed users (as of June 2026) which is up from around 6,000 in 2022. Such a large user base requires substantial moderation effort, and we have a Code of Conduct expanded with a few extra guidelines. The moderation effort is split into two teams, of which the latter is a subset of the former: the Moderators and the Code of Conduct team.

The Moderation team #

The Moderation team handles comments and messages on GitHub (within the leanprover-community organisation) and Zulip. On Zulip, this includes creating new private or public channels, organising existing channels and moving messages to their proper topic, or alerting users when a thread goes off topic or becomes otherwise unproductive. On both platforms, it entails engaging in conversations with users when they are upset by actions of others, or hiding or deleting comments violating the code of conduct. In general, the Moderation team strives to help users interact positively with the community and resolve disputes amicably wherever possible.

Users on Zulip can be suspended (temporary deactivation) by Moderators; outright bans (permanent deactivation) are implemented for sockpuppet accounts (additional accounts opened for a single individual to hide their usage). Bans for other infractions are under the purview of the Code of Conduct team. Suspension length starts at 1 day for the first violation, which may be enacted without prior warning but come with a stated reason, and doubles for successive violations. When users access the "Report message" feature on Zulip, the report, which contains the name of the reporter, is sent to the Moderators by means of a private channel, at which point the moderators may take any of the actions previously described. For a sense of scale, such actions are taken on a near-daily basis.

Because of the frequency of moderation actions, and the desire to avoid retribution directed against individual Moderators, there are a few tools available to the Moderation team to help perform some of these actions. When actions are taken by Moderators using these tools, they become public to the rest of the Moderators (because a bot posts in the private channel); and hence there is a degree of oversight of any particular moderator by the remainder of the group. Note that all these tools are triggered manually by Moderators; there is always a human in the loop. Moderation focuses primarily on clear violations of the code of conduct and Zulip guidelines, and in conflicts between individuals when all of the parties can be assumed to act in good faith.

The Code of Conduct team #

The Code of Conduct team serves a related, but slightly different purpose. While the Moderation team is large and handles the vast majority of moderation on Zulip, it is only intended for violations which are clear, or mostly clear after minor discussion amongst the remainder of the Moderation team. In contrast, the CoC team is intended to deal with situations displaying the following features:

1. Conflict between individuals which is unresolved by standard moderation.
2. Persistent disruptive behavior whose level falls below that of an unambiguous violation of the Code of Conduct.
3. Any behavior reported using the anonymous reporting form.
4. Egregious conduct worthy of a permanent ban, not only a suspension.

In short, problems handled by the Code of Conduct team constitute those which are more serious, or more persistent, or more nuanced, or require greater privacy, than those addressed by standard moderation. The Code of Conduct team, while serving as the initial point of contact for these more complicated situations and conducting discussions amongst themselves, may reach out to the wider Moderation team for input and guidance while ensuring anonymity of the original complainant. Because of the more serious and / or persistent nature of the complaints, the Code of Conduct team may also institute permanent bans, or suspensions which exceed the default doubling schedule. Bans or extra suspensions will not be implemented prior to written warning by the Code of Conduct team. As with the Moderators, the Code of Conduct team strives to help users interact positively with the community, and resolve disputes amicably wherever possible.

The Code of Conduct team will share a limited report semi-annually with the public detailing the number of complaints received, the dates of receipt, action and resolution, as well the final outcome. Detailed reasons for actions and final outcomes will be shared with relevant parties, but are not included in the semi-annual report to protect privacy.