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)
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).
one reason is likely packaging/installation and support for recent Coq. Due to tooling/libraries, they only support specific (old) Coq versions.
Thanks @Karl Palmskog. The version diff + complicated installation makes a lot of sense.
in contrast, I think CoqHammer is now very well packaged and easy to install and use (except perhaps setting up some ATPs like z3)
Yes and I presume there a numerous proofs in the coq libraries that were produced entirely with CoqHammer?
there are some, e.g., repos here https://github.com/lukaszcz
Last updated: Dec 01 2023 at 06:01 UTC