Questions on Coq

Question

Now I'm awake again, I can raise this here in meta, as per quid's request.

I commented on the question How do I verify the Coq proof of Feit-Thompson?

I like this question, and would defend it against potential voters-to-close (saying "ask in a Coq forum") by saying that this is the sort of activity (downloading and stepping through a proof certificate) that the proof assistant community, and others in the pure mathematics community (e.g. Voevodsky) are hoping would be the standard method of checking a proof in mathematics in the future

with the understanding that MO is not the place for general questions on Coq, but with the intent that if formalised mathematics is to become as important for mathematicians as its proponents hope, mathematicians need to know a little bit about the process, if not of proving theorems with the aid of proof assistants, at least of how such proofs are verified by the interested bystander. I temper this with the caveat that we can't answer (in general) questions about the nitty-gritty of Coq, but at least an 'in principle' answer should be of interest to most research mathematicians. For instance, I didn't know the mechanics as Enrico put in his answer, though I know at least a little bit of how Coq programs work (I fiddled with a few examples once, but nothing serious).

So perhaps we can discuss two things: this particular question (perhaps together with its companion question Where can I find Gonthier's Coq code proving the four color theorem?), and the general suitability of questions on formalised mathematics. I definitely think these two questions Nate has asked are interesting and on-topic, but would also limit how many we get.

History of related questions

I asked once How true are theorems proved by Coq?, but that was more obviously on-topic, and there was also Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?, but that was closed as off-topic, which I roughly agree with, as well as joro's other question on Coq (Why should I trust Coq when assumption-free proof of False in Coq exists?), which was blatantly off-topic.

Other than those, there are three other questions tagged [coq] https://mathoverflow.net/questions/tagged/coq, but they tend be more purely mathematics.

Answer 1

It is long established practice that questions related to software quite particular to mathematics are sometimes considered as on-topic and sometimes not (there are actually more questions on Coq than listed in OP, and there are still more on some proof-assistant in general, likely also not an exhaustive list; and there are numerous instances for other (mathematical) software questions like on MatLab, MAGAMA, Mathematica, Maple, Sage, GAP and so on).

The general principle being, applied with a lot of variation, that questions that also have an actual mathematical aspect to it are alright, yet that MO is not an online help-center for basic usage or installation problems with any one piece of software.

I neither see any need for having more particular or other guidelines for Coq (and also not for proof assistants in general) nor to revise this practice.

What does this mean for the particular questions.

• For the four color one, I agree with its OP that it is not really a question about Coq but a pure request for some resource, and to include it in the present discussion seems not optimal.

• For the Feit-Thompson one it likely depends how one looks at it (as often with such guidelines). In the end, the question is on the one hand popular and on the other hand harmless. And, no one voted to close (for all I can tell), no one even voted it down. Thus, I do not see any particular need to start some detailed analysis regarding its on/off-topicnes, especially now after everything is "over." (For example, I have not much problem with the question, but some of the arguments brought up in its favor seem questionable to me, yet it seems not very useful to dissect them for no particular reason.)

ps. While it is visible on main and not strictly in contradiction with the first sentence of OP, let me stress that no confusion regarding this arises: I did not request the creation of a meta thread. I requested that if OP wants to discuss the matter, then he should create a meta thread (and this after OP having posted yet one more comment in a discussion right after another one [not mine] that suggest that such discussion should go to meta).

Answer 2

I think the main thing to remember is:

This is a question-and-answer board. Not a discussion board, and not an opinion board.

So, any posting about Coq (or any other topic) should be appropriate to that model.