Stanislas Polu (Aug 17 2020 at 17:12): 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)
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).
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.
Stanislas Polu (Aug 17 2020 at 20:10):Thanks @Karl Palmskog. The version diff + complicated installation makes a lot of sense.
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)
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?
Karl Palmskog (Aug 19 2020 at 17:15):there are some, e.g., repos here https://github.com/lukaszcz
Last updated: Oct 13 2024 at 01:02 UTC