Self-Supervised Discovery of Useful Theorems in Formal Axiomatic Systems

Artificial intelligence (AI) systems have recently advanced significantly in mathematical reasoning. Many approaches, including large language models (LLMs), use human prior knowledge from mathematical text, code, or theorem libraries. Although these approaches are highly effective in practice, it remains an open question whether an agent can autonomously discover useful theorems without such human priors. To examine this question, we develop an agent for discovering useful theorems from axioms alone. Our self-supervised theorem-discovery agent alternates between proof search and useful-theorem extraction, building a library of theorems reused as lemmas for further search. The agent discovers tens of thousands of theorems across three Hilbert-style propositional axiom systems, and its classical-logic instance also proves human-written benchmark problems. Providing the discovered theorems as prompt lemmas improves proof performance across multiple external LLMs on human-written and synthetic benchmarks. The benefits are larger on harder problems and persist in our evaluation with GPT-6 Astra. Qualitative examples show that both well-known and less obvious theorems contribute to proof construction. These results show that theorem discovery without human-provided theorem or problem data can reveal useful lemmas that humans did not explicitly provide.