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
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
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
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.