Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Support for Coq #14

Open
amit9oct opened this issue Aug 5, 2023 · 1 comment
Open

Support for Coq #14

amit9oct opened this issue Aug 5, 2023 · 1 comment

Comments

@amit9oct
Copy link

amit9oct commented Aug 5, 2023 •
edited
Loading

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
Copy link
Contributor

DyeKuu commented Aug 5, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@amit9oct @DyeKuu