Proverbot9001 is an ongoing project to prove theorems in Coq automatically using machine learning and neural networks. Proverbot9001’s goal is to make foundationally verifying software more accessible to more software projects.
Proverbot9001 is free software (free as in freedom, but you also don’t need to pay anything), and is publicly available on Github. It’s still a work in progress, and as such might not be easy to set up on every machine. If you’d like to contribute, please get in touch, or send a pull request!
New: We compared Proverbot9001 to other state-of-the-art machine learning proof systems for Coq, on the CoqGym benchmark set; check it out here.
You can find out more about Proverbot9001 from our extended paper (the short version was published at MAPL 2020). You can also watch the talk in the full MAPL proceedings.
Proverbot9001 is a collaboration of Alex Sanchez-Stern, Yousef Alhessi, Sicun Gao, Lawrence Saul, and Sorin Lerner at UC San Diego.
Funded by NSF grant #1955457