We formulate learning guided Automated Theorem Proving as Partial Label Learning, building the first bridge across these fields of research and providing a theoretical framework for dealing with alternative proofs during learning. We use the plCoP theorem prover to demonstrate that methods from the Partial Label Learning literature tend to increase the performance of learning assisted theorem provers.

This document proposes an alternative proof of the result contained in article [1]. The proof is simpler to understand (I believe) and leads to a more precise statement about the asymptotical distribution of the relative amount of perturbation. Suppose that an artificial intelligent program bases its decision on the collection points neighbouring the query. Suppose that this is not the case for that query q and this collection point x . We are interested in the amount of perturbation to be applied to collection point x so that the program takes it into account.