Helping the purposed StackExchange `Proof Assistant` site

Stream: general

[Eric Taucher]

I am posting this in the general stream because Zulip asked if I wanted to notify all 5000+ users, which I obviously did not. Feel free to move this if necessary.

---

The site is currently a purposed StackExchange site and a purposed site progresses along in phases.

image.png

To reach the next phase (Commit) as @Andrej Bauer notes it needs to meet the partially completed requirement - 22 more questions with a score of 10 or more

One thing many don't realize in the current phase (Definine) is that once a sample question gets 10 votes any more votes are basically wasted. Instead vote on questions with less than 10 votes. If and when the site goes live, you can then vote for the question as you normally would at a StackExchange site. You can also change your votes to move the process along in the definition phase.

If and when the site is promoted to the Commit phase, users will have to visit the proposal again and commit to using it. This is based on a formula (ref) and existing StackExchange uses with higher rep who commit are worth more value during the commit phase.

For more details see the StackExchange Area 51 FAQ.

HTH

[Eric Wieser]

Eric Taucher said:

One thing many don't realize in the current phase (Definine) is that once a sample question gets 10 votes any more votes are basically wasted. Instead vote on questions with less than 10 votes. If and when the site goes live, you can then vote for the question as you normally would at a StackExchange site. You can also change your votes to move the process along in the definition phase.

This is sort of like studying for the exam rather than to learn the topic; the point in the voting is to establish consensus on what good and bad questions are, not just to progress to the next phase by any means necessary. If a question is particularly good, giving it extra votes above 10 is a good way to indicate that.

[Andrej Bauer]

Thank's for the support. The proposal is now the most active one in Area 51. Indeed, I think it's better to have a slower proposal procedure that clarifies things than to try to rush through by playing the system and voting for the purpose of getting to the next stage.

Note also that we do not really have enough questions, you're welcome to contribute your own.

P.S. Apologies for spamming 5000+ people in #announce , this thread is indeed a better place for discussion.

[Julian Berman]

I can't seem to log into that stack exchange, it just redirects to a page with Unable to log in: No user found :/ -- I of course have a stack exchange network user. OK, slightly counterintuitively, clicking the sign up button logged me in.

[Andrej Bauer]

I have heard of two other cases like that. Martin Escardo says the trick was to follow the advice in the last comment of https://meta.stackexchange.com/questions/319150/no-login-found-error-trying-to-log-in-at-area-51 (which is to click "Sign up" instead of "log in").

[Eric Taucher]

I did a bit more digging of what happens to questions during the commit phase. (ref)

The top example questions from the Definition phase are listed during Commitment to set the expectation and scope of what this site is about. But these are example questions and they do not automatically get posted to the site. There's more to a good question than a simple title. The folks using this site will ask about actual problems they are trying to solve. The "example questions" are little more than a vague title to help define what the site will be about.

In checking an actual site in the commit phase (ref), all of the questions with 0 or higher votes were listed. I don't know if negative questions existed.

So, learned that it advantages to ask as many questions as possible during this phase even if they gather no positive votes.

[Eric Taucher]

FYI

To undo a vote on StackExchange you click on the vote you cast (either up vote or down vote) which undoes the vote.

Many, including me years ago, thought that the way to undo a vote was to cast the opposite vote but this does not undo a vote, it changes a vote.

See: Why is it impossible to undo votes?

---

I note this because at StackExchange if you have enough reputation you can click on the vote count as see the individual up and down vote counts and I don't think all of the down votes were meant to be down votes but are incorrect undoing of votes. If this has you confused, welcome to the club.

[Bolton Bailey]

After making an account and logging in, I try to upvote some questions but it says I need to register. My profile lists my email, but says I am an "unregistered user". I click the register button, but then it says "Unable to log in: No user found". Any guidance on how to get around this?

[Bolton Bailey]

Update: The account sign up flow is weird and I think I accidentally made a second stackexchange account. I signed out and signed back in and I had my main account, after which I was able to upvote.

[Eric Taucher]

Congratulations!!!

In about 20 hours the site has moved into the next phase: Commitment

image.png

The commitment phase requires

image.png

I commit to participate actively in Proof Assistants for at least three months, especially during the private beta, and to ask or answer at least ten questions.

and suppling some simple information

1. Full name
2. Primary role/interest
3. Optional comment.

So if you can commit then you need to visit the site again, click the commit button in the upper left and provide the information. :-)

[Eric Taucher]

The Commit phase is moving along rather nicely. In particular the number of StackExchange users with 200+ rep is not lagging so far behind the other metrics that it will become an issue.

image.png

Since about half of those who signed up appear to be new to StackExchange in doing a quick search for a somewhat quick and general introduction on how such sites works I found this answer: How does Ask Ubuntu work?

As you follow along, just mentally replace Ask Ubuntu with the name for the new site Proof Assistants and it should be pretty much what to expect if and when the site reaches Beta phase.

[Eric Taucher]

For those familiar with the privileges based on rep on StackExchange sites during the Beta phases the point values are lowered but increase moving forward.

1. Private Beta (ref) - Last about 7 days but may be longer if needed.
2. Public Beta (ref) - This can last months to years, it depends on meeting the requirements.
3. Standard (ref)

This really helps those new to StackExchange sites but often comes as a shock when they loose privileges upon entering a new phase because they need more rep.

For more details see this

[Huỳnh Trần Khanh]

I think this answer raises pretty valid points. https://area51.meta.stackexchange.com/a/32595/ while i believe it's in the community's best interests to advance the site proposal, these points are worth considering IMO

[Eric Taucher]

Huỳnh Trần Khanh said:

These points are worth considering IMO

Thanks.
FYI I am Eric Taucher here and Guy Coder of Stack Exchange sites.

If you want to discuss these in detail I think it would be prudent to wait for the StackExchange site to go into Beta at which point it should/will have it's own meta site where such issues can be discussed. Also as this site (Lean Zulip) is not really the ideal place to discuss this as the users of other proof assistants are not represented here. :smile:

[Mario Carneiro]

Note that this is one of the reasons why the site was proposed in the first place - there is currently no general "proof assistants" gathering place on the internet, although this lean zulip gets a decent amount of general discussion as well

[Scott Morrison]

I have to admit I am skeptical of the proposal. SE sites have quite high "critical mass" requirements (I don't necessarily mean Area 51's requirements). To some extent the success of the zulip (and the one for coq) are actually a negative for a stack exchange site, because it would a direct "competitor".

[Scott Morrison]

Moreover, I think that for the relevant applications (learning Lean, questions about existing libraries, discussion of related theoretical issues), our present zulip community is just superior to a SE site.

[Scott Morrison]

And of course there are many things (coordinating new projects, advice to new contributors) that just make no sense on a SE site and will continue to be done here even if it is otherwise successful.

[Scott Morrison]

In my mind, the only problem a SE could usefully address is the fragmentation between languages of the Lean and Coq zulips (and, I guess, the lack of good real time communities for other languages?)

[Scott Morrison]

But I'm not totally sure that's even a problem.

[Scott Morrison]

The comparative advantage of a SE site over a zulip is essentially that SE can preserve good answers and make them accessible via Google. I'm not convinced we're "answering the same question repeatedly" enough for this to be a critical problem for our current zulip+documentation model.

[Arthur Paulino]

Even though I am very new here, I'm curious to see how it will evolve. All of it: the concept of "proof assistants", the tools involved and the community. It's reasonable to compare it with the advent of, say, object oriented programming. Things start small, almost as a prototype, and tightly structured. Then eventually it gets to the point that small groups are formed for very specific purposes (like a telegram group for an online course). Nowadays, Python, just as an example, is so big that I don't see a Zulip chat being effective. Julia might have started very small to. Same as Go.

[Patrick Massot]

I agree with Scott that we seem very far below the threshold where a SE site could become useful.

[Kevin Buzzard]

I think it might be an interesting place where people can talk about more than one prover at once

[Kevin Buzzard]

It doesn't have to be a success, it can just be an experiment.

[Yaël Dillies]

I just hope it doesn't drain our activity here.

[Eric Wieser]

I wonder if it's worth poking someone at zulip about public archives again, since the Google factor might go away if zulip handled our archiving

[Kevin Buzzard]

BTW there are many more Coq questions on stackoverflow than there are Lean questions.

[Eric Taucher]

Eric Wieser said:

I wonder if it's worth poking someone at zulip about public archives again, since the Google factor might go away if zulip handled our archiving

Is the context of this question to suggest that if Zulip did archiving then Google would index the results and thus finding the information from a Google search would be as effective as a post on a SE site?

[Kevin Buzzard]

What SE has that the archive doesn't is the upvote i.e. "this particular thing is useful" system.

[Eric Taucher]

I take it that the thumbs up indicates a yes.

Since this site (Lean Zulip) has been running fine for the needs of the community, this was not worth noting, but if one is looking at options to make the post more visible then Discourse should be put on the list.

If I seem to skip some of the dots in this please ask, this is everyday knowledge for me.
As I noted on the SE site I admin of a Discourse site with full moderator rights and then some. https://swi-prolog.discourse.group/
We are hosted for free via Discourse as part of the Free Hosting for Open Source v2. What some know but many may not is that Discourse is run by Jeff Atwood, the one who started StackOverflow (ref) and that Discourse sites hosted by Discourse seem to also share the same high ranking of Google pages. If you search for the word Prolog and some other common tech phrases it is not uncommon to find the pages from the site near the top of the Google search result.

Now for the mines in the minefield.

Our site receives so much traffic that we regularly pass the limit for being free. However another little unknow fact is that if you have an open source project you might be able to have it self-hosted for free at OSU/OSL (Oregon State University/Open Source Lab). The SWI-Prolog sites are hosted there as is a contingency site for the Discourse forum.

If as Kevin likes, one wants voting like StackOverflow, this is possible but not with the free site as those are limited to the plugins of a standard account. For more details see: Thoughts on a plugin which turns discourse into stackoverflow

If the site is self-hosted at OSU/OSL then Discourse needs a registered domain name and email service both of which AFAIK are never free for what is needed.

With my rights on the Discourse site I can see the metrics of which search engines are scanning the site. Todays result

[image.png](/user_uploads/3121/r9ZxDY725Y6hOTf2nEqDhWFB/image.png) User Agent
Mozilla/5.0 (compatible; bingbot/2.0; +http://www.bing.com/bingbot.htm)
Mozilla/5.0 (compatible; Googlebot/2.1; +http://www.google.com/bot.html)
Mozilla/5.0 (Linux; Android 6.0.1; Nexus 5X Build/MMB29P) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/96.0.4664.45 Mobile Safari/537.36 (compatible; Googlebot/2.1; +http://www.google.com/bot.html)
Mozilla/5.0 (compatible; YandexBot/3.0; +http://yandex.com/bots)
Mozilla/5.0 (Windows NT 6.1; Win64; x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/69.0.3497.81 YisouSpider/5.0 Safari/537.36
SerendeputyBot/0.8.6 (http://serendeputy.com/about/serendeputy-bot)
Mozilla/5.0 (compatible; DotBot/1.2; +https://opensiteexplorer.org/dotbot; help@moz.com)
Mozilla/5.0 AppleWebKit/537.36 (KHTML, like Gecko; compatible; Googlebot/2.1; +http://www.google.com/bot.html) Chrome/95.0.4638.69 Safari/537.36
Mozilla/5.0 (Macintosh; Intel Mac OS X 10_15_5) AppleWebKit/605.1.15 (KHTML, like Gecko) Version/13.1.1 Safari/605.1.15 (Applebot/0.1; +http://www.apple.com/go/applebot)
newspaper/0.2.8
Mozilla/5.0 (compatible; YandexBot/3.0; +http://yandex.com/bots) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/81.0.4044.268
Mozilla/5.0 (compatible; MJ12bot/v1.4.8; http://mj12bot.com/)
Mozilla/5.0 (compatible; InfoTigerBot/1.9; +https://infotiger.com/bot)
ICC-Crawler/2.0 (Mozilla-compatible; ; http://ucri.nict.go.jp/en/icccrawler.html)
YisouSpider
Mozilla/5.0 (compatible) SemanticScholarBot (+https://www.semanticscholar.org/crawler)
Mozilla/5.0 (compatible; Neevabot/1.0; +https://neeva.com/neevabot)
Mozilla/5.0 (compatible; Linux x86_64; Mail.RU_Bot/2.0; +http://go.mail.ru/help/robots)
facebookexternalhit/1.1 (+http://www.facebook.com/externalhit_uatext.php)
Mozilla/5.0 (compatible; DuckDuckGo-Favicons-Bot/1.0; +http://duckduckgo.com)
Mozilla/5.0 (compatible; HubSpot Crawler; +https://www.hubspot.com)

WhatsApp/2.21.22.26 A
Mozilla/5.0 (iPhone; CPU iPhone OS 7_0 like Mac OS X) AppleWebKit/537.51.1 (KHTML, like Gecko) Version/7.0 Mobile/11A465 Safari/9537.53 (compatible; bingbot/2.0; +http://www.bing.com/bingbot.htm)
Mozilla/5.0 (X11; Linux x86_64; HubSpot Url validation check; web-crawlers+url-validation@hubspot.com) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/51.0.2704.103 Safari/537.36
TelegramBot (like TwitterBot)
Mozilla/5.0 (Windows NT 10.0; Win64; x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/74.0.3729.169 Safari/537.36
Mozilla/5.0 (Macintosh; Intel Mac OS X 10_11_1) AppleWebKit/601.2.4 (KHTML, like Gecko) Version/9.0.1 Safari/601.2.4 facebookexternalhit/1.1 Facebot Twitterbot/1.0
Twitterbot/1.0
webprosbot/2.0 (+mailto:abuse-6337@webpros.com)
ia_archiver
Mozilla/5.0 (Morningscore/1.0)
Mozilla/5.0 (compatible; Discordbot/2.0; +https://discordapp.com)
Mozilla/5.0 (compatible; evc-batch/2.0)
node-fetch/1.0 (+https://github.com/bitinn/node-fetch)

HTH

[Mac]

I personally feel like this Stack Exchange site has the potential to draw ordinary computer science users (and students!) into proof assistants and Lean in particular. People coming from a CS background (like myself!) tend to default to Stack Exchange sites for Q&A and I know it took me a long time to seek out this Zulip and adapt to the more chatty nature of this platform as opposed to Stack Exchange's more FAQ format.

Also, I feel a lot of the coding questions that get asked in the #lean4 channel would be ripe for such a site.

[Andrej Bauer]

We're almost there! We need 10 people with reputation of 200 to commit, and 11 with any reputation. If you support the idea, please consider committing to using the site. This is especially useful if you already use any other SE site and have 200 points or more (in which case you should first Sign up to Area51 with your SE identity, then log in, and only then commit.) Thanks.

[Eric Taucher]

Some info on committing. One can only commit to three sites at a time. Years ago where there were many new sites that might be a issue and one had to be judicial, now it really does not matter. I have also committed to a few sites a while ago and then found I did not have the time to devote to fulfill the requirements. I don't recall it giving me any lasting grief. Also there are several people whom have committed who I am sure have no idea what a Proof Assistant is. Also be aware that the Sun is rising in the U.S.A and it is a Monday so we might see that last bump in the curve. :grinning:

[Patrick Massot]

Mac said:

Also, I feel a lot of the coding questions that get asked in the #lean4 channel would be ripe for such a site.

That would probably be catastrophic since the language is moving so fast. We really don't want to spend the next 10 years telling people they shouldn't read all those outdated answers.

[Mac]

@Patrick Massot That tends to be par for the course for Stack Exchange (in particular, Stack Overflow). I often stumble across answers that are hopelessly outdated. As such, I personally don't find that to be a major con. Also the beta-ness of the system fits well with beta-ness of the site! :laughing:

[Mario Carneiro]

Also you can edit posts if you want to try to keep the answers curated / up to date

[Kevin Buzzard]

you see this a lot in AskUbuntu -- "in 11.04 you do this! 29/04/11". Another answer "in 16.04 you do this! 29/04/17" etc etc.

[Huỳnh Trần Khanh]

man we are very close to the private beta :tada::tada::tada: wait wait I don't really understand area 51, what are we supposed to do in the private beta?

[Huỳnh Trần Khanh]

I'm pretty sure that Stack Exchange staff will watch our site very very closely lol :laughing: because that tends to be the case for newly created sites that gain some traction...

[Eric Taucher]

Huỳnh Trần Khanh said:

what are we supposed to do in the private beta?

In the Private Beta the rep points are lowered quite a bit, see this for details. This allows everyone in the private beta to do things they normally can't like create tags, comment everywhere, edit wikis, down vote, view close votes, vote to close and reopen, ... Also it give StackExchange a look at the community to decide if they should close the site down before making the beta public. So just jump in and take a look. Also questions asked during this period tend to get lots of votes and sometimes never get dethroned, e.g. the Prolog tag has quite a few such questions from the early days.

HTH

[Eric Taucher]

In thinking of the problem for getting 2 more in this category

98/100 committers with 200+ rep on any other site

where is it written that more people are needed.
See the solution?

[Eric Taucher]

I am pretty sure we have the needed requirements to move into Beta, it is that as some of have seen, the rep is being pulled from incorrectly. I just checked the last person (chris) to commit which shows them with a rep of 151 but checking their cs.stackexchange.com account they have 4830 rep.

[Eric Taucher]

And then it happened. :tada:

image.png

[Kevin Buzzard]

@Eric Taucher do you have any idea about whether that happened super-quickly or about as fast as average or very slowly?

[Eric Taucher]

Kevin Buzzard said:

Eric Taucher do you have any idea about whether that happened super-quickly or about as fast as average or very slowly?

IMO the speed that went from proposal to Beta would make one of Elon Musk's project look like they were standing still. If it set a record or is close to the record I would not be surprised.

Many proposals never made it out of the definition phase and many still never made it out of the commit phase. Some lingered for years. Also many sites were attempted, failed and attempted again and again. I think AI and CS went along those lines.

---

Some of the information about the sites is still accessible for reference e.g. the commit graph for the Computer Science site. (ref)

Notice that it took months to get the necessary commits. Also I asked Ken Li who made the successful proposal why he was not more active and he noted that a site for CS had been tried a few times before and noticed that it had not been attempted lately so he just tried and was lucky.

image.png

---

And as @Andrej Bauer noted, he proposed this on a weekend. So most of this was done when many don't visit such sites. I know on the Prolog site I help moderate, the post and replies drop off quite a bit on the weekends.

[Arthur Paulino]

I'm gonna be promoting Lean 4 as a tool on its early stages for general-purpose programming here in Brazil. Part of the industry is starting to shift towards the adoption of functional programming languages in production. So I'm starting early hoping to see some results in the next years. Maybe it helps populate the SE site a bit more.

[Eric Taucher]

It seems that until the site goes live for Private Beta that the commit area is still accepting users. So if you have an interest the door is still open.

[Huỳnh Trần Khanh]

hey, should we post trivial questions that can't be easily answered by searching on the internet? I plan to ask several to make it easier for new people to learn lean

[Huỳnh Trần Khanh]

for example, how would I state that there are X things that satisfy property Y in lean

[Huỳnh Trần Khanh]

(the answer is fintype.card if I'm not mistaken)

[Huỳnh Trần Khanh]

also I think we should have a documentation site with answers to these simple questions, similar to the Rust By Example website. we can copy and paste stackexchange questions and answers if these questions are widely applicable

[Huỳnh Trần Khanh]

this way anyone can edit the answers as things change

[Huỳnh Trần Khanh]

take a look: https://doc.rust-lang.org/rust-by-example/index.html this site has answers to a lot of common questions about rust and it doesn't look like an autogenerated documentation website

[Eric Taucher]

Huỳnh Trần Khanh said:

should we post trivial questions that can't be easily answered by searching on the internet? I plan to ask several to make it easier for new people to learn Lean

The best way to find out what the SE Proof Assistants community thinks and get feedback is to ask. Since the site is so new there will be lots of activity on the associated meta site for the Proof Assistants site.

[Eric Taucher]

(deleted)

[Kevin Buzzard]

I'm not sure there's much point in someone asking a question they already know the answer to

[Huỳnh Trần Khanh]

Kevin Buzzard said:

I'm not sure there's much point in someone asking a question they already know the answer to

i'm pretty sure that this is common practice on Stack Overflow to document languages and libraries that are still poorly documented elsewhere

[Huỳnh Trần Khanh]

stack exchange sites tend to rank higher on search engine results

[Huỳnh Trần Khanh]

the term for this type of question is "canonical questions" on stack overflow IIRC

[Huỳnh Trần Khanh]

https://meta.stackoverflow.com/questions/291992/what-is-a-canonical-question-answer-and-what-is-their-purpose

[Johan Commelin]

Kevin doesn't believe in the word "canonical" :rofl:

[Huỳnh Trần Khanh]

@Eric Taucher re: the deleted message, the attribution requirement can easily be fulfilled by providing a link to the original question/answer. my idea is that we can copy and paste good stackexchange questions into a dedicated documentation site where we can more easily edit and update the answers when things change, because stackexchange isn't really a good place for content that can be collectively edited

[Huỳnh Trần Khanh]

oh dear I mentioned the wrong website. I mean we can have a website similar to this https://rust-lang-nursery.github.io/rust-cookbook/intro.html

[Eric Taucher]

Huỳnh Trần Khanh said:

Eric Taucher re: the deleted message, the attribution requirement can easily be fulfilled by providing a link to the original question/answer. my idea is that we can copy and paste good stackexchange questions into a dedicated documentation site where we can more easily edit and update the answers when things change, because stackexchange isn't really a good place for content that can be collectively edited

I did not know one could see a deleted message here.

The reason I deleted the message was because I miss read your question. I thought it was asking if Q&A from SE could be copied. But upon rereading your statement you were not asking you were stating. Reading as a question I was responding, reading it as a statement needed no response.

[Andrej Bauer]

Thanks @Eric Taucher for walking us through this. It's very helpful to have someone experienced on board. Do you know how long it's going to take SE to create the private beta?

[Eric Taucher]

Andrej Bauer said:

Thanks Eric Taucher for walking us through this. It's very helpful to have someone experienced on board. Do you know how long it's going to take SE to create the private beta?

Thanks, and thanks to you and all those who committed and herded up others to commit! :+1:

---

Great question!

Short answer. I don't know but I don't recall them taking more than a few days to a week.

---

Side note 1:

If the work is being done in the U.S., Thursday is one of the major national holidays (Thanksgiving) and many people take the full week off.

Side note 2:

A few hours ago I had actually written that up as question for the SE staff on the Area 51 meta site and was ready to post it when I thought, naw others really aren't that interested as it is just my personal desire, so deleted it.

---

If you like I can ask the question of the SE staff, or you can do it.

[Eric Taucher]

One of the next major steps to be aware of is for the Moderator Pro Tempore. I don't know if the info in the link is still correct but I can ask another Ben I who I am pretty sure was appointed as one.

[Eric Taucher]

Ben I confirmed that he was and still is a moderator for the SE beta site Computer Science Educators. I have asked the obvious questions in the SE chat room named classroom. Feel free to read the messages or ask for yourself. (Note: Ben I has not responded yet so no need to check.)

[Eric Taucher]

Created SE chat room related to the proposed Proof Assistants site. As noted in the first messages,

This is just a temporary chat room for the proposed Proof Assistants site.
I say temporary because the site name might change in which case the room name would then be confusing.
:grinning:

[Eric Taucher]

FYI
Based on information from some answers and moderators at SE, the site is expected to go live on a Tuesday, 2 to 3 weeks after meeting the requirements for the Commit phase, which was Monday, 11/22/2021. The notifications for when the beta site is active are sent as an e-mail, makes sense for those joining an SE site for the first time. In researching, SE does not give an expected date because of possible unforeseen circumstances, so no need to look for one. :-)

[Théo Zimmermann]

I've seen some discussion here on making Zulip publicly visible and on Discourse. I'm going to respond to these here, but feel free to separate this in a different topic.

[Théo Zimmermann]

Regarding Zulip, the features to make it publicly visible (without registration) have been merged recently :tada: I don't know when they plan to do the next release but I hope it will be soon.

[Théo Zimmermann]

Regarding Discourse, I am the administrator of the Discourse forum for Coq (and also one of the admins for the Coq Zulip chat BTW). We created Discourse based on the successful OCaml example (and every open source community seemed to adopt this forum at that time) then (more than a year later) we created the Zulip chat based on the successful Lean (and HoTT) example.

[Théo Zimmermann]

Unfortunately, as much as I liked the Discourse forum, it seems to have never really took off. Maybe that's because we didn't officially kill the historic mailing list (Coq-Club) that it was supposed to replace in the long term at the same time.

[Théo Zimmermann]

The Zulip chat has been much more successful from the start. It currently has over twice as many subscribers as the Discourse forum. On the other hand, maybe this is partly explained by the fact that you need to subscribe to view the content, whereas you don't need to do this on Discourse... But I think this is also explained by the fact that asking a question in a chat room is less intimidating than asking a question in a forum.

[Kevin Buzzard]

Hi Théo and thanks for the observations! It is interesting that the Coq mailing list is still quite active whereas the Lean mailing list is basically dead (and if anyone asks a question on it, they're just told to go and ask at the Zulip). You might be right about the subscription thing -- I've viewed the Coq Discourse plenty of times without ever making an account there, however I have asked questions on the Coq Zulip, probsably because it was easier to do this than to make an account on the Discourse :-)

[Eric Taucher]

Yes this is going more off the topic and with the Discourse thread.
In doing a few private messages with Théo I choose to chat with him on the Coq Discourse site. To sign up I just joined, was prompted with a dialog, since I was already signed into my GitHub account clicked that and was signed up and active on the site. The whole process was faster than me typing this.

[Eric Taucher]

This post is in reference to the side topic here of making this sites information more visible and easy to find on the Internet.
This morning noticed that a post on the Discourse forum I am a member was noted on Hacker News, the site name is really very misleading, the site URL is more meaningful, news.ycombinator.com (ref). In keeping an eye on the page hits for the post, in less than an hour the count went up by another hundred. When first checked it was at 5K views and now it is at 5.1K views. It just went to 5.2K views.

[Kevin Buzzard]

Oh sure, whenever a blog post I write gets mentioned on hacker news, my blog views go through the roof.

[Eric Taucher]

Proof Assistants private beta launch will take place in January 2022

Since we want all proposals to have the best chances of thriving as possible, the Community Team has decided to postpone this proposal's launch into private beta to January 2022, in an attempt to minimize the impact of the upcoming end-of-year holidays in the site's chances of success.

Additionally, the proposal sped through its definition and commitment phases, which we believe hasn't allowed for some discussions that usually take place during those phases — such as deciding on a name and URL for the site — to come to a consensus. As such, we invite those of you who've committed to this proposal to try to have those conversations between now and the first couple of weeks of January 2022. At that time the Community Team will help y'all tie whatever loose ends need to be tied, and prepare the site for launch into private beta.

[Eric Taucher]

From SE staff member (Adam Lear) as noted in the SE chat room, We still have a few things to work our on our end, the proposal should launch in the next few weeks.

[Eric Taucher]

From JNat (Staff for Stack Exchange)
The Proof Assistants site is scheduled to launch into private beta on February 8, 2022. (ref) (Tuesday)

[Eric Taucher]

The new StackExchange site for Proof Assistants is up.

https://proofassistants.stackexchange.com/

[Julian Berman]

I'm honestly somewhat impressed at the level of activity so far, and across different communities. I was skeptical initially personally, but hopefully the momentum stays up because if so it seems this'll be a nice resource.

[Eric Taucher]

FYI

Leaving Private Beta & Initial Pro-Tem Moderator Election!

[Eric Taucher]

2022 Community Moderator Election are underway.

[Will Sawin]

No one's nominated themselves yet.

[Eric Wieser]

Is that what that means, or are nominations not shown until the elections begin?

[Will Sawin]

Eric Wieser said:

Is that what that means, or are nominations not shown until the elections begin?

I'm pretty sure nominations are shown when they happen. For example, in the recent MathOverflow election, they showed up one at a time. If this didn't happen you could end up with a situation where no one nominates themselves, or, maybe worse, only drastically unqualified users nominate themselves.

[Eric Taucher]

The election has begun. If you are curious as to who has voted you can check the badges page and look for the Constituent badge.

[Eric Taucher]

Since one needs 150 rep points to vote it seems that only 126 users can vote.

[Eric Taucher]

The election has ended. Thanks to those who ran and congratulations those who won. (ref)
Eric
Trebor
Couchy