This webpage is about Lean 3, which is **effectively obsolete**;
the community has migrated to Lean 4.

# Maintainer team

The mathlib library is under active development, with hundreds of proposed changes and additions under discussion at any time, and dozens approved every week. These proposals are structured as "pull requests" on the mathlib Github repository. The mathlib maintainers are the people who have the power to give final approval to pull requests. They must ensure mathlib has a cohesive design with a high-quality implementation.

Mathlib maintainers usually have research-level knowledge in some field of mathematics or computer science. Community members become maintainers at the invitation of the current maintainers, and anyone may nominate a community member by sending a message to a current maintainer. Maintainers serve for a renewable two-year term, with the expectation that the term will be renewed unless the maintainer has become inactive or wishes to step down.

### Members

##### Adam Topaz

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.

##### Anne Baanen

Anne is a PhD student at Vrije Universiteit Amsterdam (The Netherlands). They have been formalizing proofs in mathematics and computer science since 2018.

##### Bhavik Mehta

Bhavik is a PhD student in Mathematics at the University of Cambridge (UK). He has been formalizing mathematics since 2019.

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

##### Chris Hughes

Chris is a PhD student at INRIA with the Gallinette team in Nantes (France). He has been formalizing mathematics since 2017.

##### Eric Wieser

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.

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

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 Ebner

Gabriel is an engineer at Microsoft Research (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.

##### Heather Macbeth

Heather is an Assistant Professor of Mathematics at Fordham University (USA). She did a PhD in differential geometry in Princeton. She has been formalizing mathematics since 2019.

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

##### Kyle Miller

Kyle is a post-doc in mathematics at Université Paris-Saclay at Orsay (France). He did a PhD in low-dimensional topology at UC Berkeley. He has been formalizing mathematics since 2020.

##### Mario Carneiro

Mario is a post-doc at Carnegie Mellon University (USA). He did a PhD in pure & applied logic at CMU under Jeremy Avigad. He has been formalizing mathematics since 2013, first in Metamath and then in Lean.

##### Markus Himmel

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.

##### Oliver Nash

Oliver is a post-doc 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.

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

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

##### Riccardo Brasca

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.

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

##### Rémy Degenne

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.

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

##### Sébastien Gouëzel

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.

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