Technical Summary: Self-Supervised Theorem Discovery in a Formal Axiomatic System

Problem Statement

While recent AI systems, particularly Large Language Models (LLMs), have demonstrated significant progress in mathematical reasoning, they largely rely on human-provided priors such as mathematical text, code, and existing theorem libraries. A critical open question remains: Can an agent autonomously discover useful theorems starting solely from the primitive rules of a formal axiomatic system, without access to human prior knowledge, existing theorem libraries, or training problem sets?

Current methods often depend on human-constructed knowledge to bootstrap reasoning. Even self-improving agents in axiomatic domains often rely on external judges to evaluate the utility of discovered theorems. This paper investigates whether an agent can not only discover theorems but also identify and utilize "useful" ones to improve its own proof search and the performance of external reasoning systems, relying exclusively on axioms and inference rules.

Methodology

1. Formal Setting: Hilbert System as a Stack Machine

The authors instantiate the problem within a Hilbert axiom system for propositional logic. The system is deliberately minimal, consisting of:

• Three Axioms:
  • $Ax1: A \to (B \to A)$ (Weakening)
  • $Ax2: (A \to (B \to C)) \to ((A \to B) \to (A \to C))$ (Distribution)
  • $Ax3: (\neg A \to \neg B) \to (B \to A)$ (Contraposition)
• One Inference Rule: Modus Ponens (MP), deriving $Y$ from $X$ and $X \to Y$.

To facilitate learning, the authors formulate theorem proving as a deterministic, goal-conditioned stack-machine decision process $(S, A, s_0, P)$:

• State ($S$): A finite stack of formulas.
• Actions ($A$): Pushing instances of $Ax1, Ax2, Ax3$ onto the stack, or applying Modus Ponens (MP).
• Mechanism: The MP action uses Hindley–Milner unification. If the top stack element unifies with $X \to Y$ and the element below unifies with $X$, both are popped, and $Y$ is pushed.
• Success: A proof is successful if the stack contains a single formula matching the target goal.

2. Self-Supervised Theorem Discovery Algorithm

The core contribution is an algorithm that alternates between proof search and useful-theorem extraction, building a library of theorems that serve as lemmas for future search.

A. Goal-Conditioned Policy Learning

The agent learns a policy $\pi_\theta(A|S, g)$ to predict the next action given the current stack $S$ and a target goal $g$.

• Hindsight Learning: During a search episode, any state where the stack contains a single formula $f_t$ is treated as a "reached theorem," regardless of whether it was the original goal.
• Training Signal: The action prefix leading to $f_t$ is treated as a proof of $f_t$. These prefixes are added to a training set $D_{train}$ to update the policy via cross-entropy loss.
• Goal Buffer ($G$): A buffer maintains discovered theorems. The agent samples goals uniformly from $G$ for subsequent search episodes, effectively bootstrapping its own curriculum.

B. Extracting Useful Theorems

To prevent the library from becoming bloated with trivial or redundant theorems, the algorithm filters discovered theorems based on two criteria:

1. Generality: Theorems are filtered to remove those that are mere specializations of other candidates. The system retains only the "minimal" elements under a partial order defined by formula substitution (i.e., keeping the most general forms).
2. Reprovability: The system estimates the probability that the current policy can re-prove a theorem. Using a Bayesian posterior mean (Beta(1,1) prior), it prioritizes theorems that have been discovered but are difficult to reprove reliably. These "hard-to-reprove" theorems are valuable because adding them as lemmas compresses difficult proof paths.

C. Multi-Generation Library Expansion

The process operates in generations:

1. Policy Learning: Train the policy on the current action space (initially just axioms and MP).
2. Extraction: Identify useful theorems from the goal buffer $G$ based on generality and reprovability.
3. Action Space Expansion: Add the extracted theorems as new library actions (e.g., $Thm_1, Thm_2$). When selected, these actions push the corresponding theorem onto the stack, acting as a pre-verified lemma.
4. Iteration: Repeat the process, allowing the agent to use previously discovered theorems to find new, more complex theorems.

Key Contributions

1. Formulation: Propositional theorem proving is formulated as a stack-machine decision process directly based on Hilbert axioms and inference rules, avoiding reliance on external proof corpora.
2. Algorithm: A self-supervised theorem-discovery algorithm is proposed that grows a theorem library from primitive rules alone. It reuses extracted theorems as lemmas for subsequent proof search.
3. Autonomous Discovery: The agent discovers tens of thousands of theorems and finds proofs for human-written benchmark problems without using human priors for training.
4. Transferability: The extracted theorems serve as effective external knowledge, improving the proof performance of external LLMs when provided as prompt lemmas.

Experimental Results

1. Theorem Discovery and Coverage

• Growth: The number of discovered theorems increases over six generations, demonstrating the agent's ability to expand its knowledge base autonomously.
• Benchmark Performance: The agent successfully finds Hilbert-system proofs for 30% of a human-written benchmark set (derived from Kleene's textbook).
• Comparison: While GPT-5-high (the strongest baseline) achieves only ~23% accuracy on these benchmarks without assistance, the agent's ability to find proofs for 30% suggests it discovers non-trivial proofs that are meaningful from a human mathematical perspective.

2. Impact on LLM Reasoning

• Prompt Lemmas: When the extracted theorems are provided as prompt lemmas to GPT-4o and GPT-5 variants, their proof success rates on the benchmark problems improve significantly.
• Qualitative Analysis:
  • Some discovered theorems correspond to well-known principles (e.g., the principle of explosion, $\neg A \to (A \to B)$), which are easily interpretable.
  • Others (e.g., complex implication lifting) are not immediately obvious to humans but function effectively as supporting knowledge in LLM proofs.
  • This indicates that the agent can surface useful lemmas that humans did not explicitly provide, and these lemmas are transferable across different reasoning architectures (from the agent to LLMs).

Significance and Claims

The paper claims to provide evidence that useful theorems can emerge from proof search without relying on human-provided theorem libraries.

• Self-Evolving AI: The work suggests a path toward self-evolving AI systems for mathematics that can autonomously expand their formal knowledge through proof search while ensuring every discovery remains formally verifiable.
• Formal Verifiability: Unlike LLMs that may hallucinate plausible but incorrect statements, the agent's discoveries are strictly grounded in the axioms and inference rules of the Hilbert system.
• Modesty: The authors do not claim to have surpassed state-of-the-art LLMs in general reasoning. Instead, they demonstrate that in a constrained, formal setting, an agent can learn to discover and utilize its own knowledge to solve problems that are difficult even for advanced LLMs, and that this self-discovered knowledge can augment external systems.

The study is limited to a single axiom system (Hilbert propositional logic), but the authors posit that the framework is generalizable to richer systems like first-order logic or set theory, which remains a direction for future work.