if there was ever a clear example of a repository that would be better maintained in a community package maintenance org, I think this one is it: https://github.com/openai/miniF2F/pull/121 (employee who maintained repo quit the company)
(ideally leanprover-community org arranges the repo transfer or makes a fork)
Did you contact the lean community, like @Jason Rute ;-) . Sounds like this could help automatic translation (of statements) across systems.
The discussion on the Lean zulip about this is here: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving/topic/Meta.20IMO.20result (Well, it is on the ML for TP stream of the zulip. I don't know how many Lean users read it regularly.)
the fork at https://github.com/facebookresearch/miniF2F was mentioned, but it really doesn't solve the problem (now you have two repos with uncertain future prospects, in non-collaborative GitHub orgs)
It is probably better to have the conversation there since some people who maintain both those repos are in those conversations.
I filled in my point of view there, but unfortunately, seems that discussion got completely tangled up in the "IMO grand challenge" stuff. A general benchmark for ITP machine learning is of general interest, but I think the IMO stuff is not.
if anyone plans to do Coq-miniF2F, best thing to do is likely to fork
Last updated: Feb 05 2023 at 14:02 UTC