The talk will cover several AI methods used to learn proving of conjectures over
large formal mathematical corpora. This includes (i) machinelearning methods
that learn from previous proofs how to suggest the most relevant lemmas for
proving the next conjectures, (ii) methods that guide lowlevel proofsearch
algorithms based on previous proof traces, and (iii) methods that automatically
invent suitable theoremproving strategies on classes of problems.
I will show examples of AI systems implementing positive feedback loops between
induction and deduction, and show the performance of the current methods over
large libraries of existing proof assistants such as Isabelle, Mizar, and HOL.
Finally, I will mention emerging AI systems that combine statistical parsing of
informal mathematics with such strong theorem proving methods.
