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.
How to comment on this blog:
At present comments are disabled because the relevant script died.
If you comment on this post on Mastodon and
mention
andrejbauer@mathstodon.xyz, I will
gladly respond.
You are also welcome to contact me directly.
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.