Talia Ringer (Aug 18 2021 at 18:56): 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
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)
Gaëtan Gilbert (Aug 18 2021 at 20:15):Who's Stan?
Ali Caglayan (Aug 18 2021 at 23:12):One of the authors of miniF2F it seems
Lasse Blaauwbroek (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: Apr 20 2024 at 04:02 UTC