Simple Dataset for Proof Method Recommendation in Isabelle/HOL

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. …

Continue reading Simple Dataset for Proof Method Recommendation in Isabelle/HOL