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

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)

Who's Stan?

One of the authors of miniF2F it seems

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