Self-Supervised Theorem Discovery in a Formal Axiomatic System
Abstract Overview
This paper studies whether an agent can autonomously discover useful theorems in a formal system without relying on human-written theorem libraries, proof corpora, or natural-language supervision. The authors instantiate the problem in a Hilbert system for propositional logic and formulate proof construction as a stack-machine decision process with actions for axiom instantiation and Modus Ponens. Their self-supervised algorithm alternates between proof search and theorem extraction: formulas reached during search become future goals, and selected theorems are added back as reusable lemma actions. Across multiple generations, the method grows a theorem library, discovers tens of thousands of theorems, and produces theorems that can assist both its own search and external LLM-based proof attempts.
Novelty
The distinctive contribution is a self-supervised theorem-discovery framework that starts only from axioms and inference rules, then expands its own action space by turning discovered theorems into reusable lemma actions. The work also evaluates external utility directly by showing that discovered theorems improve LLM proof search when supplied as prompt lemmas, rather than only judging them heuristically as plausible or useful.
Results
Experimentally, the agent discovers tens of thousands of theorems over six generations and builds a final library of 38 theorem actions. The discovered set covers 30% of a 30-problem human-written benchmark in propositional logic, and the extracted theorems improve proof success for GPT-4o and GPT-5 variants when provided as prompt lemmas. Qualitative examples further show cases where GPT-5-high fails without the discovered lemmas but succeeds when they are supplied.
Key Points
- The method represents Hilbert-style theorem proving as a stack-machine process and learns a goal-conditioned policy from theorems reached during its own proof trajectories.
- Useful theorem extraction combines a generality filter with a reprovability criterion, then reinserts selected theorems as new library actions for later generations of search.
- The discovered theorems are not only internally reusable for the agent but also transferable to external LLMs, where they improve formal proof construction in the Hilbert system.