Stream: Machine learning and automation

Topic: miniF2F


view this post on Zulip 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

view this post on Zulip Notification Bot (Mar 24 2022 at 15:41):

This topic was moved here from #Miscellaneous > miniF2F by Emilio Jesús Gallego Arias.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 24 2022 at 15:51):

Yes it would, however that would apply to almost any topic

view this post on Zulip Emilio Jesús Gallego Arias (Mar 24 2022 at 15:52):

Still the post is visible in Misc

view this post on Zulip Karl Palmskog (Mar 24 2022 at 15:59):

I agree that the topic belongs here, and people can follow the trail from Misc.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Feb 06 2023 at 05:03 UTC