MiniF2F

Stream: IMO-grand-challenge

[Stanislas Polu]

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.

[Stanislas Polu]

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:

[Jason Rute]

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.

[Stanislas Polu]

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?