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 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

```latex
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.

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

Workshops and conferences #

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

Mathlib maintainers

Mathlib maintainers are community members who are actively developing mathlib and reviewing pull requests. Their number grows naturally when new users become frequent contributors.
Jeremy Avigad
													  picture
Jeremy Avigad

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 Barton
													  picture
Reid Barton

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 Carneiro
													  picture
Mario Carneiro

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
													  picture
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 Commelin
													  picture
Johan Commelin

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 van Doorn
													  picture
Floris van Doorn

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 Ebner
													  picture
Gabriel Ebner

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 Gouëzel
													  picture
Sébastien Gouëzel

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 Hudon
													  picture
Simon Hudon

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 Hughes
													  picture
Chris Hughes

Chris is an undergrad student in mathematics at Imperial College London (UK). He has been formalizing mathematics since 2017.

Yury G. Kudryashov
													  picture
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
													  picture
Robert Y. Lewis

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 Massot
													  picture
Patrick Massot

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 Morrison
													  picture
Scott Morrison

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.