Meet the community #
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 blog #
You can get news from the community on our blog.
The Lean Zulip chat #
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
```math my LaTeX code here ```
for displayed math.
If you want to participate in 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 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.
Riccardo is an Associate Professor of Mathematics at Université Paris Cité (France). He did a PhD in number theory in Milan. He has been formalizing mathematics since 2020.
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 Gin-ge Chen
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.
Rémy is a researcher at Inria Lille Nord Europe (France). He did a PhD in applied mathematics at Université de Paris. He has been formalizing mathematics since 2020.
Floris van Doorn
Floris is a post-doc in the mathematics department of the Université Paris-Saclay (France). He did a PhD in formalized mathematics and type theory at Carnegie Mellon University, and a post-doc at the University of Pittsburgh. He has been formalizing mathematics since 2011, first in Coq and now in Lean.
Frédéric is an Assistant Professor of Computer Science at the Université de Montréal. His main area of research is quantum information theory and cryptography. He has been formalizing mathematics since 2020.
Gabriel is a post-doc at Carnegie Mellon University (USA). 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 Rennes 1 (France). He did a PhD in dynamical systems in Orsay. He has been formalizing mathematics since 2016, first in Isabelle and now in Lean.
Markus is an algorithm engineer in Karlsruhe (Germany). He did a master's in pure mathematics in Cambridge (UK). He has been formalizing mathematics since 2020.
Simon is a research engineer and proof engineer at Bedrock Systems where he works on the formal verification of a novel hypervisor. He did a Master's in computer science in Zurich and started a PhD in computer science in in Toronto. Has has been involved with formal verification since 2010 including pen and paper proofs of correctness, smt-based proofs and interactive proofs with Lean and Coq. He has been writing Lean tactics since 2017.
Chris is a PhD student at INRIA with the Gallinette team in Nantes (France). He has been formalizing mathematics since 2017.
Yury G. Kudryashov
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.
Robert Y. Lewis
Rob is a lecturer in the Department of Computer Science at Brown University (USA). 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.
Bhavik is a PhD student in Mathematics at the University of Cambridge (UK). He has been formalizing mathematics since 2019.
Kyle is a post-doc in mathematics at UC Santa Cruz, previously a PhD student at UC Berkeley. He has been formalizing mathematics since 2020.
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.
Oliver is a Visiting Academic in the Department of Mathematics at Imperial College London (UK). He did a DPhil in differential geometry at Oxford (UK). He has been formalizing mathematics since 2019.
Adam is an Assistant Professor of Mathematics at the University of Alberta (Canada). His research is primarily in Galois theory and related topics from arithmetic geometry. He has been formalizing mathematics since 2020.
Eric is a PhD student at the University of Cambridge (UK). He has been formalizing mathematics since 2020, and maintaining open source software since 2017.