Abstract:
As formalization becomes a more accepted means of establishing correctness of mathematical theories, the usability of proof assistants and the automation level which they provide becomes more important. In this talk I will discuss various automated reasoning tasks that give rise to machine learning problems. First, I will present heuristic search for related mathematical knowledge. Next, we will look at the choice of the optimal strategies for proof automation.
We will continue with internal guidance, the prediction of the actual inference rules to apply at a given proof step. Finally we will look at conjecture and intermediate lemma generation.