Abstract

Interactive theorem proving has seen major development in the past decade,  and is being  widely adopted in formalisation of mathematics and in verification. Further growth and dissemination of interactive theorem proving  require more intelligent tools that can make this technology more user friendly and convenient. As full automation of interactive provers is impossible, it is important to develop better heuristics that enableto data mine the existing libraries and  reuse existing proof strategies when writing new proofs.In this talk, I will talk about several projects devoted to Machine Learning for Interactive Theorem Proving (in Coq and ACL2 )  that I participated in in the last 5 years.I will give a light survey of a variety of machine learning methods that have already been employed in these provers, and will discuss, with some help from the audience, which of those methods bear more promise for the future. In the technical part, I will also talk about ML4PG —  the machine learning extension to Proof general, that I have developed in collaboration with  my colleagues, its recent extension Coq-PR3 and the plans to re-incarnate these tools in the upcoming new version of Proof General currently developed by INRIA and at MIT .    Based on the joint work with G.Grov,  T.Gransden,  J.Heras, M.Johansson, E.McLean, N.Walkinshaw.