Code of conduct

This team handles incident reports and maintains community standards. See the community web page.


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.