Josef Urban presents Artificial Intelligence and Theorem Proving

The talk will cover several AI methods used to learn proving of conjectures over
large formal mathematical corpora. This includes (i) machine-learning methods
that learn from previous proofs how to suggest the most relevant lemmas for
proving the next conjectures, (ii) methods that guide low-level proof-search
algorithms based on previous proof traces, and (iii) methods that automatically
invent suitable theorem-proving 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.