The Lean community is rather diverse. We have users coming from computer science as well as mathematics, and even a couple of people with a physics background. Most users are either students or work in academia, but there also some data scientists and software engineers working in industry.
The main gathering point of our community is a Zulip chat instance. Since this chatroom is only visible to registered users, we provide an openly accessible archive of the public discussions. This is useful for quick reference; for a better browsing interface, and to participate in the discussions, we strongly suggest joining the chat. Registering with your real name is preferred, but not required. Starting by briefly introducing youself is also appreciated.
Questions from users at all levels of expertise are welcomed. Asking your first questions in the new members stream will ensure the answers won't asssume you know much about Lean. But you are welcome to use more specialized streams. Please start new discussion topics rather than using unrelated existing topics. If you need coding help, you may be asked to provide a 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 my_nat : n := 5 #check my_nat ```
You can use LaTeX using
$$ to enclose inline LaTeX and
```latex my LaTeX code here ```
for displayed math.
If you want to participate in our projects then you can read our contributing guide.
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 maintainer team enforces this code of conduct. Jeremy Avigad, Anne Baanen, and Simon Hudon serve as first points 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.
Mathlib maintainers are community members who are actively developing mathlib and reviewing pull requests. Their number grows naturally when new users become frequent contributors.
Maintainers have permission to merge pull requests to mathlib and access to GitHub administration settings. Otherwise they are community members like everyone else. Community decisions are discussed and made in public channels. In particular, everyone is encouraged to review pull requests and to contribute to the supporting tools for Lean and mathlib.
If you are interested in eventually joining the maintainer team, we encourage you to participate as much as possible in the review process. Please contact the current maintainers when you feel prepared.
Jeremy is a Professor of Philosophy at Carnegie Mellon University (USA). He did a PhD in mathematical logic at Berkeley, and has been formalizing mathematics since 2002, in Isabelle, Coq and Lean.
Anne is a PhD student at Vrije Universiteit Amsterdam (The Netherlands). They have been formalizing proofs in mathematics and computer science since 2018.
Reid is a post-doc at the University of Pittsburgh (USA). He did a PhD in algebraic topology in Harvard. He worked on the Glasgow Haskell Compiler, and has been formalizing mathematics since 2017.
Mario is a PhD student at Carnegie Mellon University (USA). He has been formalizing mathematics since 2013, first in metamath and then in Lean.
Bryan is a data-scientist in Dayton (USA). He did a PhD in theoretical condensed matter physics at University of Pennsylvania. He has been formalizing mathematics and helping with the community infrastructure since 2018.
Johan is a post-doc at Universität Freiburg (Germany). He did a PhD in algebraic geometry in Nijmegen. He has been formalizing mathematics since 2018.
Floris is a post-doc at the University of Pittsburgh (USA). He did a PhD in formalized mathematics and type theory in Pittsburgh. He has been formalizing mathematics since 2013.
Gabriel is a post-doc at Vrije Universiteit Amsterdam (The Netherlands). He did a PhD in computational proof theory at TU Wien (Austria). He developed the current parallel compilation infrastructure and interactive editor integration for Lean, and has been formalizing mathematics since 2016.
Sébastien is a Professor of Mathematics at Université de Nantes (France). He did a PhD in dynamical systems in Orsay. He has been formalizing mathematics since 2016, first in Isabelle and now in Lean.
Simon is a post-doc at Carnegie Mellon University (USA). He did a PhD in computer science in Toronto. He has been writing Lean tactics since 2017.
Chris is an undergrad student in mathematics at Imperial College London (UK). He has been formalizing mathematics since 2017.
Yury is a post-doc in mathematics at the Univerity of Toronto (Canada). He did a PhD in dynamical systems in Lyon and Moscow. He has been formalizing mathematics since 2019.
Rob is a post-doc at Vrije Universiteit Amsterdam (Netherlands). He did a PhD in Pure and Applied Logic at Carnegie Mellon University in Pittsburgh. He has been formalizing mathematics since 2014.
Heather is an Assistant Professor of Mathematics at Fordham University in New York (USA). She did a PhD in differential geometry in Princeton (USA). She has been formalizing mathematics since 2019.
Patrick is a Professor of Mathematics at Université Paris-Saclay at Orsay (France). He did a PhD in differential topology in Lyon. He has been formalizing mathematics since 2017.
Scott is an Associate Professor of Mathematics at the Australian National Univerity (Australia). He did a PhD in topology and category theory in Berkeley. He has been formalizing mathematics since 2017.