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

##### Anatole Dedecker

Anatole is a master's student in mathematics at Université Paris-Saclay at Orsay (France). He has been formalizing mathematics in Lean since 2020.

##### Anne Baanen

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

##### Eric Wieser

Eric is a Software Engineer at Google DeepMind. He did a PhD formalizing Clifford algebras 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 professor in the mathematics department of the University of Bonn (Germany) on formal mathematics. He did a PhD in at Carnegie Mellon University, and post-docs at the University of Pittsburgh and Université Paris-Saclay. He has been formalizing mathematics since 2011, first in Coq and now in Lean.

##### Frédéric Dupuis

Frédéric is an Associate 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.

##### Jireh Loreaux

Jireh is an Associate Professor of Mathematics in the Department of Mathematics and Statistics at Southern Illinois University Edwardsville (USA). He did a PhD in operator theory and operator algebras at the University of Cincinnati. He has been formalizing mathematics in Lean since 2018, and contributing to mathlib since 2021.

##### Johan Commelin

Johan is universitair docent (assistant professor) at Utrecht University (Netherlands) and a senior mathematical research engineer at the Lean FRO. He did a PhD in algebraic geometry in Nijmegen. He has been formalizing mathematics since 2018.

##### Joël Riou

Joël is an Associator Professor of Mathematics at Université Paris-Saclay at Orsay (France). He did a PhD in homotopy theory of schemes at Université Paris VII. He has been formalizing mathematics since 2021.

##### Kevin Buzzard

Kevin is a professor of pure mathematics at Imperial College London. He did a PhD under Richard Taylor in Cambridge UK. He has been formalising mathematics since 2017.

##### Kim Morrison

Kim is a senior research engineer at the Lean Focused Research Organization. Their background is in mathematics, particularly topology and category theory. After a PhD at Berkeley, they have worked at Microsoft Station Q, Berkeley, and the Australian National University. Kim has been formalizing mathematics in Lean and Mathlib since 2017.

##### Kyle Miller

Kyle is a post-doc in mathematics at UC Santa Cruz and a research software engineer at the Lean FRO. 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 a tech lead at the Lean FRO. He did a master's in pure mathematics in Cambridge (UK). He has been formalizing mathematics since 2020.

##### Matthew Robert Ballard

Matt is a Professor of Mathematics at the University of South Carolina (Columbia, USA). He did a PhD on derived categories in algebraic geometry at the University of Washington (Seattle, USA). He has been formalizing mathematics since 2020.

##### Oliver Nash

Oliver is a Research Engineer at Google DeepMind. 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.

##### 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 Formalization Lead at Harmonic. He did a PhD in dynamical systems in Lyon and Moscow. He has been formalizing mathematics since 2019.