Karl Palmskog (Nov 27 2022 at 00:12): Karl Palmskog (Nov 27 2022 at 00:12):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)
Karl Palmskog (Nov 27 2022 at 00:21):(ideally leanprover-community org arranges the repo transfer or makes a fork)
Bas Spitters (Nov 27 2022 at 11:25):Did you contact the lean community, like @Jason Rute ;-) . Sounds like this could help automatic translation (of statements) across systems.
Jason Rute (Nov 27 2022 at 12:31):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.)
Karl Palmskog (Nov 27 2022 at 12:43):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)
Jason Rute (Nov 27 2022 at 13:32):It is probably better to have the conversation there since some people who maintain both those repos are in those conversations.
Karl Palmskog (Nov 30 2022 at 11:35):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.
Karl Palmskog (Nov 30 2022 at 11:38):if anyone plans to do Coq-miniF2F, best thing to do is likely to fork
Last updated: Jun 03 2023 at 17:29 UTC