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.

Yutaka Nagashima will give a talk as part of the spring PL&L seminars series on Thursday the 13th of April.

Yutaka Nagashima is an Engineer at Data61, CSIRO (formerly known as NICTA).
At Data61, he developed a proof strategy language, PSL, and supported the development of certifying compiler for a purely functional programming language Cogent.
Before joining NICTA, he studied Computational Science and Engineering at Technical University Munich.

Yatuka’s homepage: https://ts.data61.csiro.au/people/?cn=Yutaka+Nagashima