Towards Smart Proof Search for Isabelle
  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.
