Are you curious about machine learning for theorem proving, but don’t know where to start?
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?
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.
Let’s get reasoning automated!