20
$\begingroup$

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.

$\endgroup$
6
  • 1
    $\begingroup$ Thanks, David. I just wanted to say that the question about the four color theorem was less about Coq and more of a reference-request, asking where I could find the code that the authors mentioned in their paper but didn't link, so I'm not sure that it really fits into this discussion. And either way this discussion comes out, I don't have any other Coq questions to ask at present, so nobody need fear a flood from me :) $\endgroup$ May 3, 2014 at 6:24
  • 1
    $\begingroup$ As it happens, I disagree with quid's comment about "bad form". As far as I know, the rough consensus about cancellation did not specify that one should wait for a vote to close before casting a vote against. $\endgroup$
    – S. Carnahan Mod
    May 3, 2014 at 6:59
  • 1
    $\begingroup$ @S.Carnahan as you know, the "cancellation" voting in comments got discontinued, among others at least so my understandingfor this precise reason. The penultimate comment the relevant tea thread (by Andrew Stacey) contains "I don't like the "pre-emptive" votes to stay open. If someone feels that a question is in danger of being closed, but no-one has actually voted to close yet then the right thing to do is start a meta thread and link to it." (cont.) $\endgroup$
    – user9072
    May 3, 2014 at 11:59
  • 1
    $\begingroup$ The final comment then was by Anton Geraschenko that basically suggested that the entire practice is abandonded and people post on meta instead. But likely I should have written some conisder it as bad form (I think I could come up with some other quotes), instead of the more assertive statement. ( @S.Carnahan ) $\endgroup$
    – user9072
    May 3, 2014 at 12:04
  • $\begingroup$ I have also posted two (or more?) Coq questions but for some reason I didn't notice there was a tag. $\endgroup$ May 4, 2014 at 4:12
  • $\begingroup$ @darijgrinberg , Nate, S. Carnahan, in case if any of you hadn't seen this yet: Stack Exchange will very soon be launching a brand new site dedicated to computer-assisted proofs: please use my referral link here if you're considering to get an invitation to the Private Beta! I also posted on Meta about this. $\endgroup$ Jan 16, 2022 at 4:54

2 Answers 2

15
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ Thanks, quid. I agree with your points, and I also agree it's better to make them here in meta. I wasn't planning for a discussion to erupt in the comments section :-) Accepting this for the sake of agreeing, other answers still welcome. $\endgroup$
    – David Roberts Mod
    May 4, 2014 at 23:51
  • 1
    $\begingroup$ Thanks for the reply. I know well how such things evolve. My initial comment was a bit rushed, and came out harsher than intended. Sorry about that. $\endgroup$
    – user9072
    May 5, 2014 at 15:09
8
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

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