search

facebookresearch / miniF2F

An updated version of miniF2F with lots of fixes and informal statements / solutions.
MIT License
58 stars 17 forks source link

Support for Coq #14

Open amit9oct opened 1 year ago

amit9oct commented 1 year ago

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 commented 1 year ago

Hello @amit9oct , there was a discussion about porting to Coq here. https://github.com/openai/miniF2F/issues/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.