2022 Moderator Election

nomination began
Mar 21, 2022 at 20:00
election began
Mar 28, 2022 at 20:00
election ended
Apr 5, 2022 at 20:00

On Stack Exchange, we believe the core moderators should come from the community, and be elected by the community itself through popular vote. We hold regular elections to determine who these community moderators will be.

Community moderators are accorded the highest level of privilege on our community, and should themselves be exemplars of positive behavior and leaders within the community.

Our general criteria for moderators is as follows:

  • patient and fair
  • leads by example
  • shows respect for their fellow community members in their actions and words
  • open to some light but firm moderation to keep the community on track and resolve (hopefully) uncommon disputes and exceptions

Full elections have three phases and an optional fourth phase (Primary):

  1. Question Collection
  2. Nomination
  3. Primary
  4. Election

Please participate in the moderator elections by voting, and perhaps even by nominating yourself to be a community moderator!

Additional Links


I'm an undergraduate at Tsinghua University,
I like mathematics and dependent type theory.

  • I'm active on this site through the beta phase. I'm also moderately active on several other Stack Exchange sites.
  • I have some experiences with proof assistants, especially those on the type theory side. See my GitHub profile.
  • I am working towards making professional knowledge more accessible to newcomers. You can see this with several of my answers and other stuff.
  • Being an undergraduate, I have a fair amount of time to spend on this site. I value this site as a place to gather and share about proof assistants. I will do all that I can to help improve both this site and its community.


I'm an Engineering PhD student at the University of Cambridge

Reasons I might make a good moderator

  • I've been active in the tag during the beta phase

  • I've over a decade of experience with StackExchange

  • I'm a maintainer for Lean's mathlib

  • I regularly interact with and help newcomers on Lean's Zulip chat.

Reasons I might not

  • I'm not that familiar with other proof assistants


I'm a PhD student. I'm interested in logic, type theory, formalizing mathematics and learning about almost every proof assistant there is.

  • I always try to be friendly and guide people in the right direction before taking direct action

  • I've been on the SE network for almost ten years. I don't post much but I'm an active user

  • This is the first site I've been active with moderation/meta/chat but I've been enjoying it


As a software developer and a math hobbyist, I am interested in formally verified software and formalization of various mathematical statements. I'm also a fan of functional programming and (dependent) type theory.

  • I'm a regular on Code Golf and Puzzling SE, and also moderately active on this site.

  • Being a hobbyist, I don't have lots of theoretical knowledge about proof assistants, but I have some experience of writing various kinds of proofs in Agda, Coq, and Lean. Codewars challenges I have written. Based on this experience, I try to answer relatively beginner-level questions when I can.

  • I try to participate in meta sites of the sites where I'm active. My meta profile on Code Golf, Puzzling, and this site.

This election is over.