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.

`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$