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](https://mattermodeling.stackexchange.com/help/badges/30/beta), then I highly recommend getting involved in the Private Beta! Questions on MathOverflow Meta and Mathematics Meta have been asked about the scope of provers: - [Questions on Coq](https://meta.mathoverflow.net/q/1672/66334) - [Tags for automated theorem provers](https://math.meta.stackexchange.com/q/12069/202425) Questions on the Theoretical Computer Science Meta have also been asked about the scope of provers: - [Questions about compilation errors in Coq](https://cstheory.meta.stackexchange.com/q/425/35155) - [Where should type-theory questions go?](https://cstheory.meta.stackexchange.com/q/1146/35155) Similar questions have also been brought up on the Meta for Computer Science SE (a very related site that a lot of the users here use): - [Are questions about software to solve computer science problems on-topic?](https://cs.meta.stackexchange.com/q/473/61663) - [Scope limits on proof assistants (e.g. Coq)](https://cs.meta.stackexchange.com/q/52/61663) - [What part of “Coq: default values for vectors” is on-topic?](https://cs.meta.stackexchange.com/q/860/61663) There was also another tangentially related Meta post on Mathematics SE: - [The problem with proof verification](https://math.meta.stackexchange.com/q/29119/202425) 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**](https://area51.stackexchange.com/proposals/126242/proof-assistants?referrer=NWYwMWI2ODE3MDgzZjk1Mzg4ZjM0MzhkMThlOGU5NWUyNTI4ZjhjOTAxNjAzMzM3ZGM5NDQxMmE2ZWI4NTdjN5SuX0TI5NhFhTPFgY_w1le8uqq_omGyNktdzn76h7sa0), 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. **[There is already a MathOverflow chat room](https://chat.stackexchange.com/rooms/131732/proofassistants-temp) which everyone here is welcome to join if they want to discuss the scope, name, or general structure of the site before it goes live!**