MiniF2F is a formal mathematics benchmark (translated across multiple formal systems) consisting of exercise statements from olympiads (AMC, AIME, IMO) as well as high-school and undergraduate maths classes.
The goal of the project is to provide a shared benchmark to evaluate and directly compare automated theorem proving systems based on the formal systems targeted, initially Lean, and Metamath (targeting also Hol Light and Isabelle). The goal would be to translate it to Coq!
This thread has been made as an extension (and from suggestions there) to crowdsource these efforts! If you have idea feel free to jump here or the issue to comment.
This topic was moved here from #Miscellaneous > miniF2F by Emilio Jesús Gallego Arias.
Ah well, sure the topic fits this stream theme, and thus is appropriate there, but #Miscellaneous has a larger audience and thus would have given more chances to the announcement to be noticed by people who are not in #Machine learning and automation.
Yes it would, however that would apply to almost any topic
Still the post is visible in Misc
I agree that the topic belongs here, and people can follow the trail from Misc.
Did anyone end up working on this? I know more people who are interested. I abandoned it because I don't really know SSReflect
I am working on this and I have a tree, but I'm on holidays now
Main blocker for it to be ready is using the new math-comp automation tactics, but I'll request for help, then it should be a matter of churning the conversion.
Last updated: Feb 06 2023 at 05:03 UTC