Zulip Chat Archive

Stream: IMO-grand-challenge

Topic: MiniF2F

view this post on Zulip Stanislas Polu (May 10 2021 at 10:29):

Cross-posting MiniF2F release announcement post: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning.20for.20Theorem.20Proving/topic/MiniF2F

We see MiniF2F as a stepping stone towards the IMO Grand Challenge, as its statements are typically much easier than IMOs, but generally still out of reach of deep-learning based automated theorem provers. We also hope that it will help foster innovation in that space by allowing direct and fair comparison between the existing methods.

view this post on Zulip Stanislas Polu (May 10 2021 at 10:30):

Unless we hear otherwise, we plan to import with proper attribution the IMOs that are in mathlib archive/ and translate them to Metamath and eventually Hol Light / Isabelle. The Lean statements of MiniF2F are under the same Apache License, so that should be no problem? :thank_you:

view this post on Zulip Jason Rute (May 10 2021 at 11:34):

It would be good to talk more about how you would like the other direction to go. Are you asking that the test theorems in MinF2F should stay out of mathlib/archive to avoid test set contamination. How about the theorems labeled valid. I think it would help to make these expectations clear.

view this post on Zulip Stanislas Polu (May 10 2021 at 11:48):

That's a great point you raise. I think it's quite easy to enforce these constraints post-hoc if one uses MiniF2F to benchmark a system, but for the things we port form mathlib we'll probably indeed focus on the valid set as a destination. If there is value porting back statements or proofs from MiniF2F to mathlib, we can probably simply agree on an easy way to tag them as such to ease their filtering for machine learning applications?

Last updated: Aug 05 2021 at 04:14 UTC