Proposal: Proof Assistants
Again it's probably better to ask in the site's meta, but I'm curious about others' opinions and thoughts on this.
- Theorem proving challenges
Informally speaking, I'm thinking of "let's prove this (mathematical or computational) statement / formalize this proof in [a proof assistant, or any proof assistant]" questions. The question would define the statement (and underlying concepts as necessary), and each answer would come up with a concrete proof coded in some proof assistant.
One concern is that there's no "most correct answer", so questions in this category are possibly "too broad".
- Code review questions
Informally, this category is for any questions that ask "I have a working code for this task, but can I improve it?".
This category already has an SE site for it, but posting one written in a proof assistant will very likely get zero answers, since proof assistant users are relatively scarce (yet). (They do have coq and lean tags, but the questions didn't go well as you can see.) On the other hand, posting on Proof Assistants has much better chance of getting good advice on improving the code (style, performance, etc.) from experts.