Stack Exchange will soon create the Private Beta site for Proof Assistants and Automatic Theorem Provers. If you want to see what a StackExchange site is like in its initial beginnings, want to help shape the future of that site, or just want the silver beta badge, then I highly recommend getting involved in the Private Beta!

Multiple questions on Computer Science Meta have been asked about the scope of provers:

Similar questions have also been brought up on the Meta for Theoretical Computer Science (a very related site that a lot of the users here use):

The question has also been raised on the Meta for MathOverflow and the Meta for Mathematics SE:

There was also another tangentially related Meta post on Mathematics SE:

Now there's finally going to be a site catering to that intersection of CS.SE, TCS.SE, MathOverflow and MSE that deals with the topic of computerized provers.

To receive updates about when the site goes live, and when it graduates, and for the opportunity to get rewarded for your early efforts with the site, you can go here, click "sign up" or "login" to make sure your Stack Exchange account is connected, the click "commit".

Often people hesitate to click "commit" because it asks you to promise that you'll post at least 10 questions or answers on the new site, but don't worry about that because most people that click "commit" do not fulfill that commitment, and there's no negative consequences for not committing. However if you do follow through with your commitment you do get rewarded for that.

  • 2
    $\begingroup$ For future reference: We allow ads for other SE sites if and only if the topic is clearly and universally relevant to the users of this site. As proof assistants and similar tools are clearly (?) a subtopic of CS, we allow the ad. Scope-related concerns are irrelevant for this decision and can be raised separately (on the Area 51 proposal). $\endgroup$
    – Raphael
    Commented Jan 17, 2022 at 11:29
  • $\begingroup$ @Raphael I only posted this here, at Theoretical CS, Math, MathOverflow and Matter Modeling (where myself and a diamond mod were early committers to the proof assistants proposal already). $\endgroup$ Commented Jan 17, 2022 at 15:29
  • $\begingroup$ @Raphael I was surprised that you felt the need to write that comment here. I posted the same thing to many other Meta sites and never got a comment even remotely like this. The ad was clearly on topic (as you yourself said), and I have shown no history of posting inappropriate ads here. However since you wrote that comment, I feel that I should ask you before posting something like this here. Programming Language Design is a sub-topic of CS, but I'm not sure whether or not you feel it's relevant enough to the users of this site. $\endgroup$ Commented Feb 6, 2023 at 5:44
  • 2
    $\begingroup$ It's been a year, and I can't claim to remember my though process back then. From my wording, I suspect I wanted to leave this note to ward off less fitting ads, as we've been getting from time to time, citing yours as precedence. Programming Language design should be fine, as well. (IMHO) $\endgroup$
    – Raphael
    Commented Feb 6, 2023 at 21:54
  • 2
    $\begingroup$ FWIW, I don't see any purpose in creating separate sites for subtopics; it only splinters the community. The metrics of Proof Assistants seem to indicate that its scope is too narrow to attract a healthy community in terms of critical mass; I predict a similar fate for Programming Language Design. That said, best of luck! $\endgroup$
    – Raphael
    Commented Feb 6, 2023 at 21:56


You must log in to answer this question.

Browse other questions tagged .