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
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 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.
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.
Leonardo de Moura
Leo is a Senior Principal Applied Scientist in the Automated Reasoning Group at AWS as well as Chief Architect and co-founder of the Lean FRO. 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.
Sebastian Ullrich
Sebastian is Head of Engineering and co-founder of the Lean FRO. He did a PhD on the Lean 4 frontend at Karlsruhe Institute of Technology (Germany). He has been working on Lean since 2015.