Stream: Machine learning and automation

Topic: CoqGym/Tactician/ProverBot proofs contributed back


view this post on Zulip Stanislas Polu (Aug 17 2020 at 17:12):

Hi everyone! Great to see this new stream!

I'm looking for references to theorems that were proved by CoqGym/ASTactic or Tactician or ProverBot9001 (or any other deep-learning based system) and whose proofs were contributed back to the Coq libraries? Git commits or email threads are all welcome. Thanks a lot!

(This question might not be exactly related to this sub-stream, happy to ask it somewhere else more adequate obviously)

view this post on Zulip Karl Palmskog (Aug 17 2020 at 17:30):

To my knowledge, these systems were only used by their authors for their respective evaluations - they haven't yet been used by regular Coq developers/engineers in verification projects (outside perhaps of some experimentation).

view this post on Zulip Karl Palmskog (Aug 17 2020 at 17:32):

one reason is likely packaging/installation and support for recent Coq. Due to tooling/libraries, they only support specific (old) Coq versions.

view this post on Zulip Stanislas Polu (Aug 17 2020 at 20:10):

Thanks @Karl Palmskog. The version diff + complicated installation makes a lot of sense.

view this post on Zulip Karl Palmskog (Aug 18 2020 at 23:21):

in contrast, I think CoqHammer is now very well packaged and easy to install and use (except perhaps setting up some ATPs like z3)

view this post on Zulip Stanislas Polu (Aug 19 2020 at 16:56):

Yes and I presume there a numerous proofs in the coq libraries that were produced entirely with CoqHammer?

view this post on Zulip Karl Palmskog (Aug 19 2020 at 17:15):

there are some, e.g., repos here https://github.com/lukaszcz


Last updated: Feb 06 2023 at 05:03 UTC