# The proposal for a proof assistants StackExchange site

- 20 November 2021
- General, Proof assistant

Proof assistant communities have grown quite a bit lately. They have active Zulip chats: Lean, Coq, Agda, Isabelle. These are good for discussions, but less so for knowledge accumulation and organization, and are not indexed by the search engines.

I have therefore created a proposal for a new “Proof assistants” StackExchange site. I believe that such a site would complement very well various Zulips dedicated to specific proof assistants. If you favor the idea, please support it by visiting the proposal and

- becoming a follower (you have to be a registered user with a verified email account),
- asking sample questions, and
- upvoting good sample questions.

To pass the first stage, we need 60 followers and 40 questions with at least 10 votes to proceed to the next stage.

##### Post a comment:

Write your comment using Markdown.
Use

`$⋯$`

for inline and `$$⋯$$`

for display LaTeX formulas,
and `<pre>⋯</pre>`

for display code. Your E-mail address is only used to compute
your Gravatar and is not stored anywhere.
Comments are moderated through pull requests.
## Comments

It would be great to have discussions related to ACL2 and its extensions as well.

Andrej, you are the founder of 21st century mathematics.