Brando Miranda (Mar 24 2022 at 15:27): Brando Miranda (Mar 24 2022 at 15:27):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.
https://github.com/openai/miniF2F/issues/66
Notification Bot (Mar 24 2022 at 15:41):This topic was moved here from #Miscellaneous > miniF2F by Emilio Jesús Gallego Arias.
Théo Zimmermann (Mar 24 2022 at 15:43):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.
Emilio Jesús Gallego Arias (Mar 24 2022 at 15:51):Yes it would, however that would apply to almost any topic
Emilio Jesús Gallego Arias (Mar 24 2022 at 15:52):Still the post is visible in Misc
Karl Palmskog (Mar 24 2022 at 15:59):I agree that the topic belongs here, and people can follow the trail from Misc.
Talia Ringer (May 09 2022 at 19:24):Did anyone end up working on this? I know more people who are interested. I abandoned it because I don't really know SSReflect
Emilio Jesús Gallego Arias (May 11 2022 at 12:05):I am working on this and I have a tree, but I'm on holidays now
Emilio Jesús Gallego Arias (May 11 2022 at 12:06):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: Oct 13 2024 at 01:02 UTC