Moderation team
The moderation team handles moderation of comments and messages on GitHub (within the leanprover-community organisation) and Zulip. On Zulip, this includes creating new private or public channels, organising existing channels and moving messages to their proper topic. On both platforms, it entails hiding or deleting comments violating the code of conduct; users on Zulip can be suspended (temporary deactivation) or banned (permanently).
The moderation team has members from Mathlib, CSLib and the broader Lean community. There's an informal distinction between Mathlib and CSLib domains: a Mathlib moderator will not moderate the CSLib channel on Zulip or the cslib repository on GitHub (and vice versa, CSLib moderators don't moderate Mathlib repositories or the mathlib channel on Zulip). The current members are the following.
Members
Adam Topaz
Adam is an Assistant Professor of Mathematics at the University of Alberta (Canada) and senior manager at the Mathlib Initiative. His research is primarily in Galois theory and related topics from arithmetic geometry. He has been formalizing mathematics since 2020.
Alexandre Rademaker
Alexandre is an Adjunct Professor at EMAp/FGV (Brazil) and the Director of CSLib Program at Renaissance Philanthropy. His research spans formal methods, theorem proving, type theory, and computational linguistics. He holds a PhD in proof theory from PUC-Rio (2010) and has been in the Lean community since 2015.
Anatole Dedecker
Anatole is a PhD student in Mathematics, specifically operator algebras, at Université Paris Cité (France). He has been formalizing mathematics in Lean since 2020.
Anne Baanen
Anne is a mathematical research engineer at the Mathlib Initiative. They did a PhD on formalizing algebraic number theory at Vrije Universiteit Amsterdam (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 senior engineer at the Mathlib Initiative. 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 Henson
Chris is a PhD student in Computer Science, specifically Programming Languages, at Drexel University (USA). In 2020 he started formalizing computer science in Lean, Rocq, and Agda while still working in quantitative finance. He has been contributing to Mathlib and CSLib since 2025.
Clark Barrett
Clark Barrett is a Professor (Research) of Computer Science at Stanford University and a member of the CSLib steering committee. He was an early pioneer in satisfiability modulo theories, formal hardware verification, and neural network verification.
Damiano Testa
Damiano is a reader in the Department of Mathematics at the University of Warwick (UK). He did a PhD in Algebraic Geometry at MIT (USA). He has been formalizing mathematics since 2020.
Eric Wieser
Eric is a Senior Software Engineer on the AlphaProof team 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.
Fabrizio Montesi
Fabrizio is professor of computer science and director at FORM, the Centre for Formal Methods and Future Computing at the University of Southern Denmark and the Danish Institute for Advanced Study. He is the pioneer of choreographic programming, lead maintainer of CSLib, and lead maintainer of the Jolie language.
Filippo A. E. Nuccio
Filippo is an Associate Professor of Mathematics at Université Jean Monnet in Saint-Étienne (France). He did a PhD in Algebraic Number Theory in Rome and has been specialising in Iwasawa theory, alongside some archimedean and non-archimedean functional analysis. As an advocate for Open Science, he is a member of MathOA and of the French Committee for Open Science. He has been formalising mathematics since 2020.
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.
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.
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 the director of the Mathlib Initiative. He did a PhD in algebraic geometry in Nijmegen. He has been formalizing mathematics since 2018.
Joël Riou
Joël is an Associate 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.
Julia Markus Himmel
Julia is a tech lead at the Lean FRO. She did a master's in pure mathematics in Cambridge (UK). She has been formalizing mathematics since 2020.
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.
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.
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.
Michael Rothgang
Michael is a postdoc in the formalised mathematics group at the university of Bonn (Germany). He did a PhD in symplectic geometry at Humboldt-Universität zu Berlin. He has been formalising mathematics since 2023.
Oliver Nash
Oliver is a mathematician who originally trained as a geometer. He is a senior manager at the Mathlib Initiative. He has spent time working in industry (proprietary trading, software), in academia (postdoc at Imperial College), and most recently spent a year as a Research Scientist 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.
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 the Inria centre at the University of Lille (France). He did a PhD in applied mathematics at Université Paris Cité. He has been formalizing mathematics since 2020.
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.
Sorrachai Yingchareonthawornchai
Sorrachai is a Junior Fellow at the Institute of Theoretical Studies, ETH Zurich. He earned his Ph.D. in Theoretical Computer Science from Aalto University (Finland) in 2023. His research focuses on graph algorithms and combinatorial optimization. He has been formalizing computer science and mathematics since 2024.
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.