Towards Smart Proof Search for Isabelle
This addresses the challenge for proof engineers in theorem proving, but it is incremental as it builds on existing methods without presenting new data or breakthroughs.
The paper tackles the problem of insufficient proof automation in theorem proving for Isabelle by proposing a proof strategy language and an AI-based approach to enhance automation, though no concrete results or numbers are provided.
Despite the recent progress in automatic theorem provers, proof engineers are still suffering from the lack of powerful proof automation. In this position paper we first report our proof strategy language based on a meta-tool approach. Then, we propose an AI-based approach to drastically improve proof automation for Isabelle, while identifying three major challenges we plan to address for this objective.