Are you curious about machine learning for theorem proving, but don’t know where to start?
Have you heard about those theorem provers with weird names, like Isabelle, Coq, and Lean?
Actually, it’s not just their names. Their internal architectures can be, … how should I say …, overwhelming, too.
Isabelle isn’t like Python or R.
You have to think about types all the time. And she comes with dozens of sub-tools called proof methods (a.k.a tactics).
You have to know when to use which method if you want to get along well with Isabelle. So, it requires a serious amount of training.
Are you scared?
Don’t worry.
We produced a simple dataset to learn when to use which proof method in Isabelle/HOL.
Our dataset is so simple that you don’t have to care about Isabelle-specific details to run your favourite ML-algorithm to learn when to use which proof method.
We are going to present this dataset at CICM2020 in July, but our draft is already available at arXiv as well as its accompanying Appendix at Zenodo, and the dataset itself at Zenodo, too.
Let’s get reasoning automated!
Regards,
Yutaka
United Reasoning 