This webpage is about Lean 3, which is effectively obsolete; the community has migrated to Lean 4.
Admin team
The admin team oversees the activities of the Lean community organization and in particular the mathlib project. It is responsible for ensuring the mathlib project continues to reflect the general views and interests of the Lean/mathlib community.
The admin team is a central hub for coordination among other teams. It is responsible for procedural duties: when a decision needs to be made, what should the process be? In particular it is tasked with finding procedures to resolve conflicts when consensus cannot be reached. The admin team also the first point of contact for the community as a whole.
The members of all teams choose an admin team annually by an election, in a manner organized by the current admin team using a system that gives all members a vote of equal weight. Members of the admin team may be re-elected.
Members
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.
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.
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.
Leonardo de Moura
Leo is a Principal Researcher in the RiSE group at Microsoft Research. He did a PhD at PUC-Rio. His research areas are automated reasoning, theorem proving, decision procedures, SAT and SMT, and he is the main architect of Z3 and of Lean.
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.
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.
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.