Are theorem proving challenges or code review questions on-topic?

Question

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.

Some concrete examples could look like these on Code Golf, minus the code golf element and (possibly) language restriction. Or like challenges on Codewars or Proving for Fun.

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.

Answer 1

Having spent a lot of time on other science/academic sites from their very beginnings, my experience tells me that inclusiveness is one of the most valuable characteristics a site can have.

Furthermore, what's the goal of the site? The site that I proposed on Area51, which is now a fully graduated site, was meant to have an impact on a certain sphere of the academic world (at least that was my intention). The more users that join, the happier I get. I cannot recall even one time where I was upset by someone coming and asking a question that I thought was too off-topic.

But, if the scope was so big that it allowed pure programming questions that have nothing to do with the academic subject, then we could get thousands of questions/day which should have been asked on StackOverflow, and then we'd get "diluted" and the enthusiasts of my subject would find the experience on the site to be a negative one (having to sift through thousands of questions they don't find interesting, to find one that interests them), and the site would succeed without those users answering questions. Fortunately that problem is not much more than hypothetical, because the askers of such questions know that they're better of asking on StackOverflow than on my site. Furthermore, I don't think that allowing questions about theorem proving strategies would dilute our community's site in the wrong way, in fact it would be quite productive to include such questions.

We are about to launch a community site which welcomes questions about automated theorem proving and proof assistants, and the suggestion for the eventual name of the site which has by far the largest number of upvotes, is Provers. I would be most happy if theorem proving challenges were to be on-topic. I teach a course on proofs at University of Waterloo, and would like to incorporate exposure to proof assistants and automated theorem provers into the course which is already all about "theorem proving challenges", and for me, all of these topics tie together, which is also why I upvoted the suggestion to name the site the "Provers Stack Exchange" or "Proofs Stack Exchange".