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.