Self-Supervised Theorem Discovery in a Formal Axiomatic System

Source: arXiv:2606.28747 · Published 2026-06-27 · By Kazuki Ota, Takayuki Osa, Tatsuya Harada

TL;DR

This paper addresses the question of whether an AI agent can autonomously discover useful mathematical theorems from scratch, without relying on any human-provided theorem libraries, training proofs, or natural language knowledge. The authors focus on the propositional logic Hilbert axiomatic system, which is minimal but formally sound and complete, and represent proof search as a sequential decision process of stack-machine actions based only on three primitive axioms and Modus Ponens. Their key innovation is a self-supervised, iterative learning algorithm that alternates between proof search and extracting useful theorems from discovered proofs. The agent maintains a growing theorem library which is reused as lemmas for future proof search to accelerate discovery. Empirically, the agent discovers tens of thousands of theorems over multiple generations, including many that can prove human-written benchmark problems in propositional logic. Further, when the discovered theorems are provided as prompt lemmas to large language models (LLMs) like GPT-5, their proof success rates on these benchmarks improve markedly. These results provide evidence that useful, human-meaningful theorems can emerge purely from formal proof search guided by self-supervised learning without any human theorem corpora, and that such theorems can serve as transferable external knowledge for other AI systems. Overall, the work suggests a promising new direction where AI systems can autonomously evolve and verify mathematical knowledge with minimal prior assumptions.

Key findings

• The agent discovered and accumulated tens of thousands of theorems over six generations of iterative proof search and theorem extraction (Fig 4).
• On a benchmark of 30 human-written propositional logic problems from Kleene’s textbook, the agent found Hilbert-system proofs for 30% of the problems (Fig 5).
• GPT-5-high baseline found only about 23% of these benchmark problems without lemma augmentation, indicating difficulty of the task in Hilbert system (Fig 5).
• Providing theorems discovered by the agent as prompt lemmas improved proof success rates for GPT-4o and all GPT-5 variants on the benchmark problems (Fig 6).
• Theorem extraction uses a combined criterion of generality (removing specialized variants) and low reproving reliability, selecting 38 theorems over generations as reusable lemmas.
• A concrete example showed GPT-5-high succeeded on proving A →(¬A →B) only after being given two extracted theorems (Thm1 and Thm2) as lemmas, illustrating their concrete proof utility (Tables 1 and 2).
• The proof search and policy learning process uses a goal-conditioned policy that learns from its own reached theorems as training goals via supervised learning from proof prefixes (Algorithm 1).
• The stack-machine action space is progressively expanded with discovered theorem actions that push lemmas onto the stack, enabling reuse and compression of proofs (Algorithm 2).

Threat model

n/a — The paper does not address security or adversarial threat models. The system operates in a closed formal environment without adversarial interference.

Methodology — deep read

1. Threat Model & Assumptions: The adversary model is implicit — there is no adversarial interference assumed. The system starts with only the three primitive axioms and the Modus Ponens inference rule of the Hilbert propositional logic system. It does not use any human-curated theorem libraries, proof corpora, natural language data, or external supervision. The goal is to discover useful theorems autonomously from this minimal primitive base. The adversary capabilities are irrelevant since the focus is on autonomous discovery and reuse.

2. Data: The environment is the formal Hilbert axiomatic system for propositional logic, with formulas built only from implication (→) and falsity (⊥). No external training dataset or human problem statements are used for training. Human-written benchmark problems (30 problems) are used only for evaluation, independently of training or library construction. The proof search agent collects sets of discovered theorems (formulas appearing on the stack as single formulas in proof episodes) which are stored in a goal buffer G used as training goals.

3. Architecture/Algorithm: Proof search is formulated as a deterministic, goal-conditioned Markov decision process where states are finite stacks of formulas and actions are pushing axioms Ax1–Ax3 or applying Modus Ponens (MP). The agent learns a policy π_θ(A | S, g) using a goal-conditioned supervised learning approach. Training data are generated by relabelling each reached single-formula stack encountered during proof search episodes as a new goal. Proof prefixes leading to that theorem become supervised data for π_θ.

The method alternates between training the goal-conditioned policy on the current action space and extracting useful theorems from recently reached buffered goals. Extraction involves filtering for generality (discarding specialized variants) and ranking by low reprovability (theorems previously discovered but difficult to reprove reliably). The selected theorems are added as new lemma actions expanding the action space. This creates multi-generation library growth where the policy learns to reuse previously discovered lemmas.

4. Training Regime: The method is run for six generations; in each generation a new policy is trained from scratch or from previous iteration using the current action space. Within each generation, many proof search episodes are run, sampling goals uniformly from the goal buffer. Training batches are constructed from proof prefixes leading to reached theorems. Hyperparameters such as batch size, epochs, or network architecture details are not explicitly detailed in the paper. The policy is optimized with cross-entropy loss.

5. Evaluation Protocol: Proof success is measured on 30 human-written benchmark propositional logic problems from Kleene (curated by Poesia et al.). A problem is solved if a generated action sequence produces a valid proof verified by a stack-machine checker under the Hilbert system with added lemma actions. Baseline comparisons include multiple GPT versions (GPT-4o, GPT-5 low/medium/high) attempting the same proofs without and with prompt lemmas. Reproducibility relies on the exact stack-machine rules and policy learning described, but code and weights are not explicitly released. There is no open distribution shift or adversarial robustness testing.

6. Reproducibility: The paper does not explicitly mention code release or frozen weights. The underlying Hilbert system and stack-machine decision process is a standard formal system and the method is algorithmically described in detail (Algorithms 1 and 2). The human benchmark is public from prior work. However, exact training seeds, network architectures, hardware, and hyperparameters for reproducibility are not fully specified.

Example end-to-end: At generation 1, the action space contains Ax1, Ax2, Ax3, and MP only. The agent runs many proof search episodes targeting goals sampled from its initial goal buffer (bootstrapped with random rollouts), collecting reached single-formula states as theorems. Using these proofs as supervised examples, the policy is updated to better choose actions for proving sampled goals. After many iterations, a set of theorems discovered is filtered by generality and reprovability, generating ~20 useful theorems added to the action space as lemma-pushing actions before generation 2 begins. In generation 2, the policy learns over this expanded action space, enabling proofs that reuse these lemmas, discovering even more theorems. This iterative process yields a growing library and improved proving ability, culminating in coverage of 30% of human problems.

Overall, the method tightly integrates symbolic proof search, self-supervised goal-conditioned policy learning, and iterative lemma extraction/reuse within the minimal Hilbert axiom system formalized as a stack-machine.

Technical innovations

• Formulating Hilbert-system propositional theorem proving as a goal-conditioned sequential decision process on a stack machine with action primitives for axioms and Modus Ponens.
• A self-supervised training algorithm using reached single-formula stacks as relabeled goals for goal-conditioned supervised learning, without external proof data or reward signals.
• A theorem extraction method combining generality-based filtering of specialized formulas and Bayesian-estimated reprovability to select useful lemmas from self-discovered theorems.
• Multi-generation iterative theorem library expansion by adding extracted useful theorems as new stack-machine actions, enabling lemma reuse to accelerate future proof search.
• Demonstrating that the discovered theorems improve external large language model (LLM) proof search when supplied as prompt lemmas, thus transferring knowledge across architectures.

Datasets

• Human-written propositional logic benchmark problems from Kleene (1952), curated by Poesia et al. (2024) — 30 problems — public

Baselines vs proposed

• GPT-5-high baseline: proof success on Kleene benchmark = ~23% without lemmas vs 30% for the proposed agent
• GPT-4o baseline: proof success improves when provided extracted theorems as prompt lemmas (exact numbers shown in Fig 6, e.g., increase from ~5% to ~15%)
• GPT-5 variants (low, medium, high): all show improved proof success rates with extracted lemmas, quantitatively shown in Fig 6

Figures from the paper

Figures are reproduced from the source paper for academic discussion. Original copyright: the paper authors. See arXiv:2606.28747.

Fig 2: Stack-machine execution for the proof tree of A →A. The proof tree in Figure 1 is converted into a linear action sequence:

Fig 3: An example proof-search episode used to generate goals and training data. Marked states are single-formula stacks, and the

Fig 4: Number of discovered theorems in the Hilbert axiom

Fig 5: Proof success rates on human-written benchmark prob-

Fig 6: compares the proof success rate with and without

Limitations

• Experiments restricted to a single minimal formal system — the Hilbert axiom system for propositional logic; applicability to richer logics remains untested.
• Details about neural network architecture, training hyperparameters, and computational resources are sparse, limiting reproducibility.
• No adversarial or distribution shift testing of the discovered theorems or learned policies.
• Human-written benchmark problems used only for evaluation; evaluation breadth is limited to 30 problems in propositional logic.
• The approach currently scales to relatively small problems; scalability to larger or first-order logic theorem proving is uncertain.
• Theoretical guarantees on convergence or completeness are not provided, though soundness and completeness of the Hilbert system are known.

Open questions / follow-ons

• Can this self-supervised theorem discovery approach scale effectively to richer formal systems, such as first-order logic or set theory?
• How well do the discovered theorems transfer as lemmas to other theorem proving systems beyond Hilbert systems or to other reasoning agents?
• What are the limits of autonomous lemma discovery without access to human-constructed proofs or external knowledge for more complex mathematics?
• Can integrating this theorem discovery algorithm with large language models lead to hybrid systems that combine formal verification with natural language math reasoning?

Why it matters for bot defense

For bot-defense and CAPTCHA practitioners interested in formal methods, this paper provides a novel approach to autonomously discovering provable lemmas from minimal logical rules without relying on external human datasets. The use of a goal-conditioned policy trained via self-supervised learning to search proof spaces could inspire automated synthesis of domain-specific logical invariants or challenge-response puzzles rooted in provable properties. Moreover, the demonstrated transfer of discovered lemmas to external LLM-based proof systems suggests a pathway to develop formal knowledge bases that augment language models for verification of challenge logic. While this work focuses on propositional logic rather than security protocols or authentication logic, its framework for iterative theorem library growth and lemma reuse highlights a promising paradigm for formal verification techniques in bot-detection mechanisms, where provable guarantees about challenge hardness or bot behavior invariants may be needed. However, the current method’s limited scope to propositional Hilbert systems means applications to more expressive formalisms relevant in security remain an open research direction.

Cite

@article{arxiv2606_28747,
  title={ Self-Supervised Theorem Discovery in a Formal Axiomatic System },
  author={ Kazuki Ota and Takayuki Osa and Tatsuya Harada },
  journal={arXiv preprint arXiv:2606.28747},
  year={ 2026 },
  url={https://arxiv.org/abs/2606.28747}
}

Read the full paper

• arXiv:2606.28747 (abstract)
• arXiv:2606.28747 (PDF)