Despite the recent progress in automatic theorem provers, proof engineers are still suffering from the lack of powerful proof automation.
In this talk, I present a proof strategy language for Isabelle and a proof method recommendation tool we are developing at Data61.
Then, I sketch a smart proof search tool based on these two predecessors to drastically improve proof automation for Isabelle,
while identifying major challenges we have to address for this objective.