Support for Coq

[amit9oct]

Is there any effort for writing these formulations in Coq? I'm not sure if all these problems can be formulated using mathcomp or if we need some other Coq library. Any particular reason for not having formulations in Coq?

[DyeKuu]

Hello @amit9oct , there was a discussion about porting to Coq here. openai/miniF2F#66 I'm not sure if the libraries needed to formalize these statements are ready there as they are quite exercise-oriented rather than theorem oriented and I'm not familiar with Coq.