Proposal: Proof assistants

Looking at the requirements for proof assistants, I'm a skeptical that it would be considered a "healthy" site by StackExchange. Looking at the sites that are already in Beta gives some requirements:

10 questions per day on average is a healthy beta, 5 questions or fewer per day needs some work. A healthy site generates lots of good content to make sure users keep coming back.

90% answered is a healthy beta, 80% answered needs some work. In the beta it's especially important that when new visitors ask questions they usually get a good answer.

Every site needs a solid group of core users to assist in moderating the site. We recommend: 150 users with 200+ rep (currently 346 users with 200+ rep) 10 users with 2,000+ rep (currently 34 users with 2,000+ rep) 5 users with 3,000+ rep (currently 23 users with 3,000+ rep)

2.5 answers per question is good, only 1 answer per question needs some work. On a healthy site, questions receive multiple answers and the best answer is voted to the top.

1,500 visits per day is good, 500 visits per day needs some work. A great site benefits people outside the community. Eventually, 90% of a site's traffic should come from search engines.

I don't know how much traffic the Lean Zulip has, but I don't know if Agda could average 10 per day.

  • 2
    There are 61 sample questions created under the proposal in 2 days. Let's see how far we can go
    – ice1000
    Commented Nov 20, 2021 at 21:22
  • 1
    I 2nd the view of @ice1000 the glass is not half empty, nor is it half full, as I noted elsewhere only time will tell.
    – Guy Coder
    Commented Nov 20, 2021 at 21:48
  • 2
    One point that may work in favor of needing many questions is that Lean is becoming a stable of University classes and those of us with a long history on StackOverflow know how many questions university students can generate in a day.
    – Guy Coder
    Commented Nov 20, 2021 at 21:50
  • 4
    @GuyCoder: be careful what you wish for ;-) Commented Nov 20, 2021 at 22:16
  • 1
    @AndrejBauer Que Sera, Sera
    – Guy Coder
    Commented Nov 20, 2021 at 22:18
  • 2
    In preparation for my Lean course in the maths department at Imperial I've been asking a bunch of (not necessarily mathematics) undergraduates how they learn programming languages and the response was pretty unanimous: they go for it, and if they get stuck they google for help. This is the reason that the current system (a ton of Zulips) is not a good fit for broadening the appeal of this growing area and in particular making it accessible to young people. Stackexchange sites have very high google visibility. Closed you-have-to-log-in-to-see-this-stuff Zulips don't. Commented Nov 21, 2021 at 13:51

2 Answers 2


It's worth noting that these criteria (like much of Area 51) are fairly out of date. In particular, there seems to be less of an emphasis on the rate of Q&A or the size of a site and more on whether it will build up a dedicated community. So questions per day, answers per question, and even (to an extent) visits per day are not weighted as heavily, while having a consistent community of users and getting most questions answered is considered important.

As a case in point, a number of Beta sites were recently informed that they would graduate in December. The known criteria for this were:

  1. The site needed to exist for at least 6 months
  2. The site needed at least 1000 open questions
  3. Of those open questions, 70% needed to have an upvoted answer.

These were the stats to graduate, so there are plenty of Beta sites that don't even meet these fairly lax requirements. So I don't think the traffic requirements are nearly as stringent now as they were back in the day.

  • 2
    Also AI will graduate despite not meeting those requirements. Commented Nov 21, 2021 at 2:50

I consider frequently visiting this site. Mostly planning to ask questions that collect up when trying to implement these things. There are already few sample questions up I would have asked.

But you'll likely see "Are dependent types the only way ahead?" and "how to embed linear types into a proof checker?"

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .