8

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.

6
  • 2
    There are 61 sample questions created under the proposal in 2 days. Let's see how far we can go
    – ice1000
    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
    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
    Nov 20, 2021 at 21:50
  • 4
    @GuyCoder: be careful what you wish for ;-)
    – Andrej Bauer
    Nov 20, 2021 at 22:16
  • 1
    @AndrejBauer Que Sera, Sera
    – Guy Coder
    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.
    – Kevin Buzzard
    Nov 21, 2021 at 13:51

2 Answers 2

Reset to default
10

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.

1
  • 2
    Also AI will graduate despite not meeting those requirements.
    – Nike Dattani
    Nov 21, 2021 at 2:50
2

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 .