There are comments suggesting that the question Formalization of unsolved problems should be closed because it doesn't contain the big-list tag. I don't understand this. Am I missing something?

First, I think it is a legitimate question. I think there are only two small issues:

  • It could be more clear that it is talking about unsolved problems in mathematics (like the RH) compared to unsolved problems in proof assistants (like FLT).
  • It is a bit similar to Libraries of formally stated theorems with proofs verified by humans and maybe that makes it a duplicate. (I don't think it is, but maybe that other question nonetheless answers this one.)

I also don't see why it is "way too open ended" or needs a big-list tag. I think if such a library exists (which it probably doesn't) there would only be one or two such examples. I don't think every question of the form "is there a proof assistant which does X?" or "is there a library of X?" needs a big-list tag.

But maybe I'm not looking at this the right way.

  • $\begingroup$ Also, if the question is still up after I end work today and not closed or already answered, I'll give my best shot at an answer. $\endgroup$
    – Jason Rute
    Mar 22, 2022 at 13:12
  • $\begingroup$ Ok, I was conflating the two issues. Sorry for that. But I'm still not sure why it was too open? Or even how it could be narrowed down in a way that doesn't change its meaning entirely. I would concede that if the OP provided more motivation for why they want a list, that might help (and that is good advice for all OPs). $\endgroup$
    – Jason Rute
    Mar 22, 2022 at 14:16
  • $\begingroup$ (By "list" I meant "library".) $\endgroup$
    – Jason Rute
    Mar 22, 2022 at 14:31
  • 1
    $\begingroup$ I don't see any problem with the linked question. It doesn't need a big-list tag and I don't see what the "focus" problem is: as asked it has a simple yes/no answer, and if the answer is "yes", a link to such a project can be given. Andrej has already given such an answer. $\endgroup$
    – Josh
    Mar 22, 2022 at 17:18
  • $\begingroup$ Just to add some context as the author of that question originally, my intent was not to get a list of libraries. My intent was to establish whether there is any such library. I also don't think the question is particularly open ended, other than the fact that if there are multiple such libraries, then any of them would suffice as an answer. $\endgroup$
    – Reubend
    Mar 24, 2022 at 5:28


You must log in to answer this question.

Browse other questions tagged .