Is there a library (for any proof assistant) which provides formalized definitions of unsolved problems? To clarify, I mean some collection that correctly defines unsolved problems in the language of a proof assistant, without attempting to provide any solutions.
By unsolved problems, I mean one which haven't been solved by any human mathematician (like the Riemann hypothesis) rather than just ones which have been proven but not formalized in a proof assistant.
