Usefulness-Driven Learning of Formal Mathematics

Creating an AI that can truly “do” mathematics requires more than just solving isolated problems: it must be able to progressively build up a corpora of useful knowledge in a similar manner as do mathematicians. To this end, we introduce UseFor, a novel framework to formalize this notion of building up knowledge, and demonstrate how it can be used to train a usefulness-driven AI mathematician. UseFor determines a theorem’s usefulness based on two criteria: its reusability in subsequent proofs and its contribution to increasing proof likelihood. We integrate UseFor into the self-play conjecturing-and-proving setting of Minimo, training a model from scratch through a conjecturing and proving self-play loop with usefulness testing. We experimentally evaluate this usefulness-driven self-play approach across three mathematical domains: arithmetic, propositional logic, and group theory with two metrics: intrinsic usefulness, a measure of how often the lemmas are used, and extrinsic usefulness, a measure driven by LLM evaluation. Our results demonstrate that our usefulness-trained model effectively generates a large number of intrinsically and extrinsically useful formal theorems.