This webpage is about Lean 3, which is effectively obsolete; the community has migrated to Lean 4.
Code of conduct
This team handles incident reports and maintains community standards. See the community web page.
Members
![Anne Baanen picture](/img/anne.jpg)
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.
![Jeremy Avigad picture](/img/jeremy.png)
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.
![Simon Hudon picture](/img/Simon.jpg)
Simon Hudon
Simon is a research engineer and proof engineer at Bedrock Systems where he works on the formal verification of a novel hypervisor. He did a Master's in computer science in Zurich and started a PhD in computer science in in Toronto. Has has been involved with formal verification since 2010 including pen and paper proofs of correctness, smt-based proofs and interactive proofs with Lean and Coq. He has been writing Lean tactics since 2017.