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.