Stream: Coq devs & plugin devs

Topic: miniF2F


view this post on Zulip Talia Ringer (Aug 18 2021 at 18:56):

Hey, openAI made a benchmark suite for mathematical proofs across proof assistants: https://github.com/openai/miniF2F. One future application of this FWIG is translation between proof assistants by way of a language model, which sounds fantastic for interoperability. It would be really nice to have a community effort to add proofs for Coq here, if Stan is OK with that

view this post on Zulip Talia Ringer (Aug 18 2021 at 18:57):

Without that, we could expect Coq to get left out of a lot of the industrial efforts involving neural networks for proof synthesis and translation, which honestly will just mean Coq getting left behind eventually, since neural proof synthesis is eventually going to work pretty well (much less naively than it's currently done, but the potential is there)

view this post on Zulip Gaƫtan Gilbert (Aug 18 2021 at 20:15):

Who's Stan?

view this post on Zulip Ali Caglayan (Aug 18 2021 at 23:12):

One of the authors of miniF2F it seems

view this post on Zulip Lasse (Aug 19 2021 at 01:00):

With the Lean to Coq translator, this may not even be very hard to do: https://coq.discourse.group/t/alpha-announcement-coq-is-a-lean-typechecker/581 (I'm not sure if this is in a state where it can be seriously used)


Last updated: Oct 16 2021 at 02:03 UTC