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.

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.

If you want to participate in our projects then you can read our contributing guide.

In addition to general formal methods conferences such as CPP and ITP, the Lean community gathers at specific events. The largest past events were:

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.

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.

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.