10

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.

5
  • 1
    Theorem proving challenges Since you seek others' opinions I would probably just avoid such questions if they were allowed. If I were to get a vote on the decision it would be no. If I were a moderator on the site I would accept that they are what the community likes and support it as best as possible.
    – Guy Coder
    Dec 17 '21 at 11:34
  • 1
    Code review questions. Since you seek others' opinions. While I know other sites such as StackOverflow migrate such questions to the Code Review site, I would be in favor that such question remain for this site and be tagged as such. I think such questions are not only a good fit for the site but a valuable dimension for others to learn. Since Prolog is my main tag of use on SO, when I see Prolog type review questions migrated to the Review site I know that they tend not to get the same attention as if they stayed on StackOverflow.
    – Guy Coder
    Dec 17 '21 at 11:40
  • 2
    As another example outside of Code Golf, Chemistry has had some success with synthesis golf questions, where users compete to make a molecule in as few synthetic steps as possible. It might not be something you want to start day one, but it could be the sort of question you ask to bump up traffic during slower months of the year.
    – Tyberius
    Dec 17 '21 at 21:03
  • I think the analogous questions would be, "How would you go about formalizing X? What are the different ways to formalize X? What are the advantages and disadvantages to [approach]?" Dec 18 '21 at 20:17
  • What about code golf implementations of provers, like Let there be HOL Light? Jan 15 at 19:29
-3

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".

1
  • 1
    Gah, sorry, I haven't been sleeping well and mistook tabs. On a more relevant note, I agree with your thoughts (and kinda fear some theorem prover communities will be hostile to the endeavour). Dec 22 '21 at 3:56

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .