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.