Self-Supervised Theorem Discovery in a Formal Axiomatic System

# Self-Supervised Theorem Discovery in a Formal Axiomatic System
Source: [https://arxiv.org/html/2606.28747](https://arxiv.org/html/2606.28747)
###### Abstract

Recent artificial intelligence \(AI\) systems have shown remarkable progress in mathematical reasoning\. Many existing approaches, including large language models \(LLMs\), draw on human prior knowledge in the form of 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\. We study this question in a formal axiomatic system by developing an agent that starts from axioms and inference rules alone and gradually grows a library of useful theorems\. Concretely, we propose a self\-supervised theorem\-discovery algorithm that alternates between proof search and useful\-theorem extraction, building a theorem library whose entries are reused as lemmas for subsequent proof search\. Experiments show that the agent discovers tens of thousands of theorems and finds proofs for human\-written benchmark problems, suggesting that its discoveries include theorems meaningful from a human mathematical perspective\. Furthermore, the discovered theorems improve LLM proof performance when provided as prompt lemmas, indicating that they can serve as external knowledge for LLM reasoning\. Our results provide evidence that useful theorems can emerge from proof search without relying on human\-provided theorem libraries\. More broadly, they suggest a path toward self\-evolving AI systems for mathematics whose discoveries remain formally verifiable\.

Machine Learning, Automated Theorem Proving, Mathematical Reasoning

\\icml@noticeprintedtrue††footnotetext:\\Notice@String

## 1Introduction

Artificial intelligence \(AI\) systems are rapidly improving their mathematical reasoning abilities\. Large language models \(LLMs\) such as GPT and Gemini have shown steady gains on mathematical benchmarks\(OpenAI,[2024b](https://arxiv.org/html/2606.28747#bib.bib32),[2025](https://arxiv.org/html/2606.28747#bib.bib35); Gemini Team,[2025](https://arxiv.org/html/2606.28747#bib.bib36)\)\. A recent Gemini model was also reported to achieve gold\-medal standard performance at the International Mathematical Olympiad 2025\(Luong and Lockhart,[2025](https://arxiv.org/html/2606.28747#bib.bib40)\), highlighting advances in LLM\-based mathematical reasoning\.

Although LLMs can perform mathematical reasoning in natural language, their outputs can be difficult to verify because they may contain plausible but incorrect statements caused by hallucination\(Farquharet al\.,[2024](https://arxiv.org/html/2606.28747#bib.bib41); Kalaiet al\.,[2025](https://arxiv.org/html/2606.28747#bib.bib42)\)\. This has motivated work on theorem proving with formal languages and proof assistants as a path toward rigorous mathematical reasoning\. Recent work includes autoformalization and proof sketching methods that connect natural\-language mathematics to formal proofs\(Wuet al\.,[2022](https://arxiv.org/html/2606.28747#bib.bib22); Jianget al\.,[2023](https://arxiv.org/html/2606.28747#bib.bib29)\), methods for generating proofs in proof assistants such as Lean\(Hanet al\.,[2022](https://arxiv.org/html/2606.28747#bib.bib20); Poluet al\.,[2023](https://arxiv.org/html/2606.28747#bib.bib21); Yanget al\.,[2023](https://arxiv.org/html/2606.28747#bib.bib23); Xinet al\.,[2024](https://arxiv.org/html/2606.28747#bib.bib44); Zimmeret al\.,[2025](https://arxiv.org/html/2606.28747#bib.bib45); Hubertet al\.,[2026](https://arxiv.org/html/2606.28747#bib.bib46)\), and methods that combine language\-model generation with symbolic reasoning or learned libraries\(Trinhet al\.,[2024](https://arxiv.org/html/2606.28747#bib.bib47); Wanget al\.,[2024](https://arxiv.org/html/2606.28747#bib.bib43); Dong and Ma,[2025](https://arxiv.org/html/2606.28747#bib.bib50)\)\. This line of work highlights the value of combining formally verifiable reasoning substrates with the search capabilities of machine learning models\.

At the same time, many current methods start from mathematical knowledge constructed by humans\. For example, mathematical language models may use natural\-language mathematical knowledge through pretraining on mathematical text and code\(Azerbayevet al\.,[2024](https://arxiv.org/html/2606.28747#bib.bib31)\), and methods that connect natural language to formal proofs often start from human\-written problem statements or informal proofs\(Wuet al\.,[2022](https://arxiv.org/html/2606.28747#bib.bib22); Jianget al\.,[2023](https://arxiv.org/html/2606.28747#bib.bib29)\)\. In addition, methods for proof generation and retrieval\-augmented theorem proving often use existing formal libraries and the theorems and proofs contained in them\(Hanet al\.,[2022](https://arxiv.org/html/2606.28747#bib.bib20); Poluet al\.,[2023](https://arxiv.org/html/2606.28747#bib.bib21); Yanget al\.,[2023](https://arxiv.org/html/2606.28747#bib.bib23)\)\. Even methods based on large\-scale synthetic data often construct training data from natural\-language mathematical problems\(Xinet al\.,[2024](https://arxiv.org/html/2606.28747#bib.bib44)\)\. Such knowledge is highly useful in practice, but it makes it difficult to isolate the question of how much mathematical structure an agent can discover from formal rules alone\.

A related line reduces reliance on human\-provided proofs or existing data by learning from axioms and formal rules\(Wuet al\.,[2021](https://arxiv.org/html/2606.28747#bib.bib25); Laurent and Platzer,[2022](https://arxiv.org/html/2606.28747#bib.bib30); Poesiaet al\.,[2024](https://arxiv.org/html/2606.28747#bib.bib49)\)\. These studies show that agents can self\-improve in axiomatized domains and discover theorems or proofs\.Kasrielet al\.\([2025](https://arxiv.org/html/2606.28747#bib.bib51)\)is especially close, as it discovers theorems from axioms, reuses them for further search, and evaluates external usefulness by asking an LLM judge whether they appear useful\. However, it remains open whether such theorems can improve an external reasoning agent’s proof performance when supplied as lemmas\. We address this question and show that the theorems discovered by our approach improve both the agent’s own proof search and LLM proof search\.

In this study, we ask whether an agent can autonomously discover useful theorems without relying on human prior knowledge\. To isolate this question, we require the agent to start only from the primitive rules of a formal axiomatic system, without using an existing theorem library, a proof corpus, natural\-language priors, or an externally provided training problem set\. Human\-written problems are used only for evaluation, not for training the agent or constructing the theorem library\.

We instantiate this formal\-system setting in a Hilbert axiom system for propositional logic\. This setting is deliberately minimal: it has only a few primitive rules, but proof search is still nontrivial and every discovered theorem remains formally checkable\. Specifically, we formulate Hilbert\-system proof search as a stack\-machine decision process, where the state is the current proof stack and the actions push Hilbert axioms onto the stack or apply Modus Ponens\. Because formulas obtained during search can be regarded as theorems, proof search itself generates theorem candidates\.

On top of this stack\-machine formulation, we propose a self\-supervised theorem\-discovery algorithm that grows a theorem library from the agent’s own proof search\. The agent reuses theorems reached during search as future proof goals and learns a goal\-conditioned policy from the action sequences that reach them\. The supervision comes from the agent’s own successful proof prefixes: whenever search reaches a theorem, the corresponding action sequence becomes a training signal for proving that theorem again\. It then extracts useful theorems from the discovered set and adds them as theorem actions that can be used as lemmas in later generations of proof search\. In this way, the agent learns not only to discover theorems, but also to use them to prove new theorems\.

Experiments show that the proposed method discovers theorems that are useful both for the agent’s own proof search and for proof search by external LLMs\. Specifically, the agent discovers tens of thousands of theorems and finds proofs for human\-written benchmark problems\. Moreover, the extracted theorems improve LLM proof performance when provided as prompt lemmas\. These results show that useful theorems can emerge from proof search based only on axioms and inference rules, and that they can serve not only as internal lemmas for the agent but also as knowledge that assists external reasoning systems\.

Our contributions can be summarized as follows:

1\.We formulate propositional theorem proving as a stack\-machine decision process based directly on the axioms and the inference rule of a Hilbert axiom system\.2\.We propose a self\-supervised theorem\-discovery algorithm that grows a theorem library from the primitive rules of a Hilbert axiom system and then reuses extracted theorems as lemmas for further proof search\.3\.Our experiments show that our agent discovers tens of thousands of theorems and finds proofs for human\-written benchmark problems\.4\.Finally, we show that the extracted theorems also improve LLM proof performance when provided as prompt lemmas, serving as external knowledge for LLM reasoning\.

## 2Preliminaries

![Refer to caption](https://arxiv.org/html/2606.28747v1/x1.png)Figure 1:Hilbert system and proof tree forA→AA\\to A\. Top: the three axioms and Modus Ponens\. The axioms respectively mean weakening, distribution of implication, and contraposition\. Bottom: a proof tree derivingA→AA\\to Afrom twoAx1instances, oneAx2instance, and two Modus Ponens steps\.This section defines the logical setting used throughout the paper\. It provides the basis for the stack\-machine decision process introduced in Section[3](https://arxiv.org/html/2606.28747#S3)\.

#### Notation for Propositional Formulas\.

To keep syntax simple, this paper builds formulas only from implication→\\toand falsity⊥\\bot\. Standard presentations often use primitive connectives such as negation¬\\neg, conjunction∧\\land, disjunction∨\\lor, implication→\\to, and biconditional↔\\leftrightarrow\. For expressive power in classical propositional logic, these connectives need not all be primitive, since implication and falsity form a basis for the usual connectives\(Post,[1921](https://arxiv.org/html/2606.28747#bib.bib9)\)\. Concretely, define¬A:=A→⊥\\neg A:=A\\to\\bot,A∨B:=\(A→⊥\)→BA\\lor B:=\(A\\to\\bot\)\\to B, andA∧B:=\(A→\(B→⊥\)\)→⊥A\\land B:=\(A\\to\(B\\to\\bot\)\)\\to\\bot\. DefineA↔BA\\leftrightarrow Bas\(A→B\)∧\(B→A\)\(A\\to B\)\\land\(B\\to A\), expanded using conjunction\. Thus, unless otherwise stated, every formula uses only→\\toand⊥\\bot, and other connectives are syntactic sugar expanded by the translations above\.

#### Rules of the Hilbert System\.

A Hilbert system is an axiomatic proof system in which theorems are derived from axioms using inference rules\(Hilbert and Ackermann,[1950](https://arxiv.org/html/2606.28747#bib.bib11); Mendelson,[2015](https://arxiv.org/html/2606.28747#bib.bib10)\)\. The system used in this paper, shown in Figure[1](https://arxiv.org/html/2606.28747#S2.F1), consists of three axioms,Ax1,Ax2,Ax3, and one inference rule, Modus Ponens\. The symbolsA,B,CA,B,Cin the axioms stand for arbitrary formulas\. A proof repeatedly introduces axioms and applies Modus Ponens, which derivesYYfrom previously obtained formulasXXandX→YX\\to Y\. When the final formula matches the target, it has been derived as a theorem\. The bottom panel of Figure[1](https://arxiv.org/html/2606.28747#S2.F1)shows a proof tree for the theoremA→AA\\to A\. It uses two instances ofAx1, one instance ofAx2, and two applications of Modus Ponens\. In this way, a Hilbert system proves theorems by combining axioms and inference rules\.

#### Soundness and Completeness\.

This Hilbert system is known to be sound and complete for classical propositional logic\(Church,[1996](https://arxiv.org/html/2606.28747#bib.bib12)\)\. Soundness means that every formula derived in this system is valid under the standard semantics of classical propositional logic\. Completeness gives the converse guarantee, namely every formula valid in classical propositional logic can be derived in this Hilbert system\. These properties justify viewing the Hilbert system as one of the standard axiomatic systems for classical propositional logic\.

#### Difficulty of Finding Proofs\.

While soundness and completeness guarantee correctness and existence of proofs, they do not imply that proofs are easy to find\. Indeed, deciding propositional validity is a coNP\-complete problem\(Cook,[1971](https://arxiv.org/html/2606.28747#bib.bib13)\)\. Moreover, from the perspective of proof complexity, valid formulas need not have short proofs in a given proof system, and proof length can vary substantially across proof systems\(Cook and Reckhow,[1979](https://arxiv.org/html/2606.28747#bib.bib14)\)\. Therefore, efficiently finding proofs in the Hilbert system is a nontrivial problem\.

## 3Stack\-Machine Formulation of Theorem Proving

![Refer to caption](https://arxiv.org/html/2606.28747v1/figures/stack_machine_sgm.png)Figure 2:Stack\-machine execution for the proof tree ofA→AA\\to A\. The proof tree in Figure[1](https://arxiv.org/html/2606.28747#S2.F1)is converted into a linear action sequence: axiom instances at the leaves are executed as push actionsAx1,Ax2, andAx3, and internal Modus Ponens nodes are executed asMPactions\. EachMPaction pops an implication and its antecedent from the stack and pushes the corresponding consequent\. This example shows that the five\-action sequenceAx1,Ax1,Ax2,MP,MPis a proof ofA→AA\\to A\.We formulate proof construction in the Hilbert system as an action sequence executed by a stack machine\. A Hilbert proof is usually represented as a proof tree built from axioms and Modus Ponens\. For a learning algorithm, however, it is more natural to represent proof construction as a sequential decision process\. We therefore flatten proof trees into sequences of stack operations\.

Formally, for a target formulagg, we define the stack\-machine decision process as a deterministic, goal\-conditioned decision process given by the tuple\(𝒮,𝒜,s0,P\)\(\\mathcal\{S\},\\mathcal\{A\},s\_\{0\},P\), where𝒮\\mathcal\{S\}is the set of finite stacks of formulas,𝒜=\{𝙰𝚡𝟷,𝙰𝚡𝟸,𝙰𝚡𝟹,𝙼𝙿\}\\mathcal\{A\}=\\\{\\mathtt\{Ax1\},\\mathtt\{Ax2\},\\mathtt\{Ax3\},\\mathtt\{MP\}\\\}is the action space, and the initial states0s\_\{0\}is the empty stack\. The transition rulePPis deterministic\. Each axiom action pushes the corresponding Hilbert axiom schema onto the stack\. For theMPaction, we use Hindley–Milner unification over formula metavariables\(Hindley,[1969](https://arxiv.org/html/2606.28747#bib.bib15); Milner,[1978](https://arxiv.org/html/2606.28747#bib.bib16); Damas and Milner,[1982](https://arxiv.org/html/2606.28747#bib.bib17)\)\. If the top formula can be unified with an implicationX→YX\\to Yand the formula immediately below it can be unified withXX, then theMPaction is legal and, when applied, pops both formulas and pushes the resulting consequentYY\. The process succeeds for goalggwhen the stack consists of the single formulagg\. We do not specify a scalar reward function in this formulation, because the learning signals in our method are constructed from self\-discovered theorems rather than externally defined rewards\.

Figure[2](https://arxiv.org/html/2606.28747#S3.F2)illustrates this view by showing the proof tree forA→AA\\to Aas a stack\-machine execution\. In this example, twoAx1actions, oneAx2action, and two Modus Ponens actions produce the theoremA→AA\\to Aon the stack\. Following this stack\-machine decision process, Hilbert\-style theorem proving can be treated as a sequential decision problem in which the agent chooses which axiom to introduce and when to apply Modus Ponens\.

## 4Self\-Supervised Theorem Discovery

In this section, we describe how the proposed algorithm operates on the stack\-machine decision process formulated in Section[3](https://arxiv.org/html/2606.28747#S3)and how it reuses discovered theorems in subsequent proof search\. The central idea is to construct learning signals from the agent’s own search trajectories, rather than relying on external proof data or human\-provided lemmas\. Specifically, the policy is learned from self\-discovered theorems through goal\-conditioned supervised learning\. In addition, the algorithm extracts theorems that are difficult to reprove and highly general, and adds them as new actions so that they can be reused as lemmas in subsequent search\. We describe these components in the following subsections\.

### 4\.1Learning a Goal\-Conditioned Policy from Self\-Discovered Theorems

The proposed method learns a goal\-conditioned policyπθ​\(A\|S,g\)\\pi\_\{\\theta\}\(A\|S,g\), whereSSis the current proof stack,ggis the target theorem, andAAis a stack\-machine action\. Here,AAeither introducesAx1,Ax2, orAx3, or appliesMP\. The policy therefore predicts which action should be taken next to prove the goal formulaggfrom the current stackSS\.

During search, any state whose stack contains a single formula yields a reached theorem\. If the stateStS\_\{t\}contains only one formulaftf\_\{t\}at timett, we callStS\_\{t\}a single\-formula stack and treatftf\_\{t\}as a theorem reached in that episode, regardless of whether it matches the original goal formulagg\. Thus, even a failed attempt can provide a learning signal when a single\-formula stack appears\.

![Refer to caption](https://arxiv.org/html/2606.28747v1/x2.png)Figure 3:An example proof\-search episode used to generate goals and training data\. Marked states are single\-formula stacks, and the corresponding formulasf1f\_\{1\},f3f\_\{3\}, andf7f\_\{7\}are added to the goal buffer𝒢\\mathcal\{G\}\. For each reached theorem, we use all preceding state\-action prefixes as training examples:𝒟train←𝒟train∪\(∪t∈\{1,3,7\}\{\(St′,At′,ft\)∣0≤t′<t\}\)\\mathcal\{D\}\_\{\\mathrm\{train\}\}\\leftarrow\\mathcal\{D\}\_\{\\mathrm\{train\}\}\\cup\\left\(\\cup\_\{t\\in\\\{1,3,7\\\}\}\\\{\(S\_\{t^\{\\prime\}\},A\_\{t^\{\\prime\}\},f\_\{t\}\)\\mid 0\\leq t^\{\\prime\}<t\\\}\\right\)\.Figure[3](https://arxiv.org/html/2606.28747#S4.F3)illustrates this construction\. The marked statesS1S\_\{1\},S3S\_\{3\}, andS7S\_\{7\}containf1f\_\{1\},f3f\_\{3\}, andf7f\_\{7\}, and the corresponding action prefixes are proofs of those formulas\. These reached theorems are then used in two ways, as future goals and as supervised training data\.

We maintain a goal buffer𝒢\\mathcal\{G\}containing theorems discovered during search\. Training begins by bootstrapping𝒢\\mathcal\{G\}with random rollouts\. Whenever search produces new reached theorems, they are added to𝒢\\mathcal\{G\}, and later iterations sample a goal formulagguniformly from𝒢\\mathcal\{G\}before rolling out the current policyπθ\(⋅\|S,g\)\\pi\_\{\\theta\}\(\\cdot\|S,g\)\.

Reached theorems also define supervised targets for the current policy update\. Whenftf\_\{t\}is reached at timett, the prefix up tottis treated as a proof offtf\_\{t\}, and for each0≤t′<t0\\leq t^\{\\prime\}<twe add\(St′,At′,ft\)\(S\_\{t^\{\\prime\}\},A\_\{t^\{\\prime\}\},f\_\{t\}\)to𝒟train\\mathcal\{D\}\_\{\\mathrm\{train\}\}\. The policyπθ​\(A\|S,g\)\\pi\_\{\\theta\}\(A\|S,g\)is then updated by cross\-entropy on𝒟train\\mathcal\{D\}\_\{\\mathrm\{train\}\}, increasing the likelihood ofπθ​\(At′\|St′,ft\)\\pi\_\{\\theta\}\(A\_\{t^\{\\prime\}\}\|S\_\{t^\{\\prime\}\},f\_\{t\}\)\.

Algorithm[1](https://arxiv.org/html/2606.28747#alg1)summarizes this procedure for a fixed action space\. It makes explicit that each reached theorem is inserted into two objects with different roles\. The training set𝒟train\\mathcal\{D\}\_\{\\mathrm\{train\}\}stores proof\-labeled examples for the current policy update and is reset at each iteration\. In contrast, the goal buffer𝒢\\mathcal\{G\}is maintained across iterations, so the agent gradually expands the set of goals available for later search\. This separation keeps policy updates local to the current iteration while preserving discovered theorems as persistent future goals\.

Algorithm 1Policy Learning in a Fixed Action Space1:Input:action space

𝒜\\mathcal\{A\}\.

2:Initialize a new policy

πθ​\(A\|S,g\)\\pi\_\{\\theta\}\(A\|S,g\)for

𝒜\\mathcal\{A\}\.

3:Bootstrap the goal buffer

𝒢\\mathcal\{G\}with random rollouts\.

4:foreach iterationdo

5:Initialize current training set

𝒟train←∅\\mathcal\{D\}\_\{\\mathrm\{train\}\}\\leftarrow\\emptyset\.

6:foreach episodedo

7:Sample a goal formula

gguniformly from

𝒢\\mathcal\{G\}\.

8:Roll out

πθ\(⋅\|S,g\)\\pi\_\{\\theta\}\(\\cdot\|S,g\)for

TTsteps\.

9:foreach reached theorem

ftf\_\{t\}at time

ttdo

10:Add

ftf\_\{t\}to

𝒢\\mathcal\{G\}\.

11:Add proof\-prefix examples for

ftf\_\{t\}to

𝒟train\\mathcal\{D\}\_\{\\mathrm\{train\}\}\.

12:endfor

13:endfor

14:Update

πθ\\pi\_\{\\theta\}by cross\-entropy on

𝒟train\\mathcal\{D\}\_\{\\mathrm\{train\}\}\.

15:endfor

16:Return:goal buffer

𝒢\\mathcal\{G\}\.

Our method shares with Hindsight Experience Replay \(HER\) and goal\-conditioned supervised learning \(GCSL\) the idea of reusing what was actually reached in past trajectories as new goals\(Andrychowiczet al\.,[2017](https://arxiv.org/html/2606.28747#bib.bib28); Ghoshet al\.,[2021](https://arxiv.org/html/2606.28747#bib.bib27)\)\. The difference is that the relabeled goals are not environment states, but proved theorems obtained as single\-formula stacks in the Hilbert system\. Thus, formulas encountered during exploration can be reused as valid theorem\-proving targets in subsequent search\.

### 4\.2Extracting Useful Theorems

We extract useful theorems from the discovered theorem set using two criteria, generality and reprovability\. The goal buffer𝒢\\mathcal\{G\}constructed in the previous section serves as the candidate set\. Generality removes overly specialized theorems, while reprovability prioritizes theorems that have already been discovered but cannot be reliably reproved by the current policy\. Adding such theorems as lemmas can expand the set of theorems reached in subsequent proof search\.

The first criterion uses the generality order induced by substituting formulas for variables to remove overly specialized theorems\. For example, the theoremA→AA\\to Ais more general than the theorem\(A→B\)→\(A→B\)\(A\\to B\)\\to\(A\\to B\), because substituting the formulaA→BA\\to BforAAin the former yields the latter, whereas no variable substitution in the latter yields the former\. We keep only the theorems that are not specializations of other candidates\. Formally, we define a partial order so that more general theorems are smaller, and retain the minimal elements under this order\. This filtering removes redundant specialized theorems while retaining more general candidates\.

The second criterion ranks the remaining candidates by estimating how reliably the current policy can reprove them\. For each candidate theoremg∈𝒢g\\in\\mathcal\{G\}, we record the numberngn\_\{g\}of timesggwas sampled as a proof goal and the numbermgm\_\{g\}of those episodes in whichggwas proved\. A theorem with low reprovability has already been discovered, but the current policy cannot reliably prove it again\. Making such a theorem available as a lemma can compress a difficult partial proof into a single lemma call\. To estimate reprovability, we use the Bayesian posterior meanp^g=\(mg\+1\)/\(ng\+2\)\\hat\{p\}\_\{g\}=\(m\_\{g\}\+1\)/\(n\_\{g\}\+2\), which corresponds to a Beta\(1,1\)\(1,1\)prior, rather than the raw empirical success rate\. This smoothing prevents the ranking from over\-prioritizing theorems that fail after only a few samples and helps identify theorems with persistently low reprovability\.

Finally, generality filtering and reprovability ranking are combined to select useful theorems from𝒢\\mathcal\{G\}\. The method first keeps only the theorems that are not specializations of other candidates, thereby removing redundant specializations\. It then sorts the remaining candidates so that lower values of the reprovability posterior meanp^g\\hat\{p\}\_\{g\}receive higher priority\. Finally, a fixed number of the highest\-priority theorems are selected from this ranking and regarded as useful theorems\.

![Refer to caption](https://arxiv.org/html/2606.28747v1/figures/found_theorems_by_generation_an_axiom_system.png)Figure 4:Number of discovered theorems in the Hilbert axiom system\. The count increases over generations, indicating that the agent can grow a theorem library within the Hilbert axiom system\.
![Refer to caption](https://arxiv.org/html/2606.28747v1/figures/success_rate_gpt.png)Figure 5:Proof success rates on human\-written benchmark problems\. Our agent finds Hilbert\-system proofs for 30% of them, while GPT baselines indicate the difficulty of the task\.

### 4\.3Reusing Useful Theorems

The proposed method reuses extracted theorems by adding them to the action space of the stack\-machine decision process\. The original action space consists of four actions: pushing an instance ofAx1,Ax2, orAx3onto the stack, and applying the inference ruleMP\. For each extracted theorem, we add one library action, denoted by𝚃𝚑𝚖𝟷,𝚃𝚑𝚖𝟸,…,𝚃𝚑𝚖𝙽\\mathtt\{Thm1\},\\mathtt\{Thm2\},\\ldots,\\mathtt\{ThmN\}\. When one of these theorem actions is selected, the corresponding theorem is pushed onto the stack instead of an axiom\. The resulting stack\-machine decision process allows the agent to reuse theorems discovered in earlier generations as lemmas in later proof search\.

Algorithm[2](https://arxiv.org/html/2606.28747#alg2)summarizes how the action space is expanded across generations\. The algorithm alternates between policy learning under a fixed action space and action\-space expansion using extracted theorems\. In each generation, we train a new policy network for the current action space, because adding library actions changes the action space of the stack\-machine decision process\. During policy learning, reached theorems accumulate in the goal buffer𝒢\\mathcal\{G\}through multiple iterations of proof search and supervised updates\. At the end of the generation, useful theorems are extracted from𝒢\\mathcal\{G\}, and the corresponding library actions are added to the action space𝒜\\mathcal\{A\}\. This process turns theorems discovered in one generation into reusable action primitives for later generations\. By repeating this process, the agent gradually expands its action space and grows a library of useful theorems\.

Algorithm 2Multi\-Generation Library Expansion1:Initialize action space

𝒜←\{𝙰𝚡𝟷,𝙰𝚡𝟸,𝙰𝚡𝟹,𝙼𝙿\}\\mathcal\{A\}\\leftarrow\\\{\\mathtt\{Ax1\},\\mathtt\{Ax2\},\\mathtt\{Ax3\},\\mathtt\{MP\}\\\}\.

2:foreach generationdo

3:Give

𝒜\\mathcal\{A\}to Algorithm[1](https://arxiv.org/html/2606.28747#alg1)and obtain theorem buffer

𝒢\\mathcal\{G\}\.

4:Extract useful theorems

\{𝚃𝚑𝚖𝟷,…,𝚃𝚑𝚖𝙽\}\\\{\\mathtt\{Thm1\},\\ldots,\\mathtt\{ThmN\}\\\}from

𝒢\\mathcal\{G\}\.

5:Expand

𝒜←𝒜∪\{𝚃𝚑𝚖𝟷,…,𝚃𝚑𝚖𝙽\}\\mathcal\{A\}\\leftarrow\\mathcal\{A\}\\cup\\\{\\mathtt\{Thm1\},\\ldots,\\mathtt\{ThmN\}\\\}\.

6:endfor

## 5Experiments

### 5\.1Experimental Setup

Table 1:Qualitative examples in which GPT\-5\-high failed without prompt lemmas but succeeded when supplied with extracted theorem actions\. The last column lists the theorem actions used in each successful proof\.Table 2:Extracted theorem actions appearing in the successful qualitative proofs in Table[1](https://arxiv.org/html/2606.28747#S5.T1)\. Each action label denotes a discovered theorem supplied to GPT\-5\-high as a prompt lemma\.We run theorem discovery and library construction in the Hilbert axiom system shown in Figure[1](https://arxiv.org/html/2606.28747#S2.F1)\. The initial action space consists ofAx1,Ax2,Ax3, andMP\. Thus, before any library theorem is extracted, the agent can only push instances of the three axioms onto the stack or apply Modus Ponens\. We repeat proof search and library extraction over six generations\. The numbers of extracted theorems added to the library are20,10,5,2,1,020,10,5,2,1,0from Generation 1 to Generation 6, which yields a final library of3838theorem actions\.

For benchmark evaluation, we use the3030human\-written propositional\-logic problems derived from Kleene’s textbook\(Kleene,[1952](https://arxiv.org/html/2606.28747#bib.bib52)\)and curated byPoesiaet al\.\([2024](https://arxiv.org/html/2606.28747#bib.bib49)\)\. This benchmark provides a human\-written test set that is independent of our theorem\-discovery process\. Each LLM baseline is evaluated once per problem with fixed decoding settings, so the reported success rates reflect single\-shot proof generation rather than best\-of\-kksampling\. A problem is counted as solved only when the generated action sequence is accepted by a stack\-machine proof checker implementingAx1–Ax3, theorem actions, and Modus Ponens with the same unification rule as in Section[3](https://arxiv.org/html/2606.28747#S3)\. In the lemma\-augmented setting, each theorem action pushes the corresponding theorem from the extracted library onto the stack\. Since each extracted theorem is stored with its primitive axiom/MPproof trajectory, lemma\-augmented proofs can in principle be expanded into axiom\-only Hilbert proofs\.

### 5\.2Quantitative Evaluation of Theorem Discovery

We first evaluate whether the proposed method can grow the goal buffer𝒢\\mathcal\{G\}starting only from the axioms and inference rule of the Hilbert axiom system defined in Section[2](https://arxiv.org/html/2606.28747#S2)\.

Figure[5](https://arxiv.org/html/2606.28747#S4.F5)shows that the number of discovered theorems increases over generations\. This result demonstrates that our approach accumulates found theorems and reuses them to derive further theorems within the formal axiomatic system\.

We next evaluate coverage on the human\-written benchmark problems\. Discovering many theorems alone does not guarantee that they are meaningful from a human perspective\. This benchmark consists of classical\-logic problems\. As shown in Figure[5](https://arxiv.org/html/2606.28747#S4.F5), the discovered theorem set covers30%30\\%of these benchmark problems\. This result suggests that the agent does not merely generate many theorems, but also discovers theorems that are meaningful from a human perspective\.

We further evaluate the difficulty of solving these benchmark problems in the Hilbert system using LLM baselines\. Figure[5](https://arxiv.org/html/2606.28747#S4.F5)shows the fraction of benchmark problems for which each GPT baseline\(OpenAI,[2023](https://arxiv.org/html/2606.28747#bib.bib33),[2024a](https://arxiv.org/html/2606.28747#bib.bib34),[2025](https://arxiv.org/html/2606.28747#bib.bib35)\)finds a Hilbert\-system proof path\. For GPT\-5, low, medium, and high denote the reasoning effort used at inference time\. Even GPT\-5\-high, the strongest GPT baseline in our evaluation, reaches only about23%23\\%accuracy, which indicates that constructing Hilbert\-system proofs for these benchmark theorems is nontrivial\. Here, we do not aim to claim that the proposed method generally outperforms state\-of\-the\-art LLMs\. Rather, these results show that the benchmark problems are difficult to solve in the Hilbert system and indicate that our approach can discover nontrivial proofs\.

### 5\.3Quantitative Evaluation of Extracted Theorems

We evaluate whether the extracted theorems also function as external knowledge for LLM proof search\. Specifically, we provide the extracted theorems as prompt lemmas and compare the proof success rate of GPT baselines on human\-written benchmark problems\. This evaluation tests whether theorems obtained by our proof\-search agent can transfer to LLMs, which rely on a different reasoning architecture\.

Figure[6](https://arxiv.org/html/2606.28747#S5.F6)compares the proof success rate with and without the extracted theorems provided as prompt lemmas\. For GPT\-4o and the GPT\-5 variants, proof success rates improve when the extracted theorems are provided as prompt lemmas\. This result shows that the extracted theorems can help LLMs find proofs in the Hilbert system\. Overall, these results show that theorems extracted through our approach function as transferable knowledge for LLM\-based theorem proving\.

![Refer to caption](https://arxiv.org/html/2606.28747v1/figures/lemma_success_rate_comparison_gpt.png)Figure 6:Effect of extracted theorems as prompt lemmas for LLM proof search\. Providing extracted theorems improves proof success rates for GPT\-4o and GPT\-5 variants\.
### 5\.4Qualitative Analysis of Extracted Theorems

Finally, we examine concrete examples of how extracted theorems assist LLM proof construction\. Table[1](https://arxiv.org/html/2606.28747#S5.T1)summarizes three goals for which GPT\-5\-high failed to find a proof without prompt lemmas but succeeded when the extracted theorem library was supplied\. Table[2](https://arxiv.org/html/2606.28747#S5.T2)lists the extracted theorem actions that appear in these successful proofs\.

The first example is especially informative because the two lemmas used in the proof have different roles\. With the extracted theorems provided as prompt lemmas, GPT\-5\-high constructed the following Hilbert\-system proof action sequence:

𝙰𝚡𝟷,𝚃𝚑𝚖𝟷,𝚃𝚑𝚖𝟸,𝙼𝙿,𝙰𝚡𝟸,𝙼𝙿,𝙼𝙿\.\\mathtt\{Ax1\},\\mathtt\{Thm1\},\\mathtt\{Thm2\},\\mathtt\{MP\},\\mathtt\{Ax2\},\\mathtt\{MP\},\\mathtt\{MP\}\.
In this proof,Thm1corresponds to the principle of explosion, deriving an arbitraryBBfrom¬A\\neg AandAA\. Thus, the usefulness ofThm1is easy to interpret from a human perspective\. In contrast,Thm2does not appear among the human\-written benchmark problems and was discovered by our approach\. Although its usefulness is not obvious at first glance,Thm2lifts an implication under an additional context and contributes to proving the first goal in Table[1](https://arxiv.org/html/2606.28747#S5.T1)when combined withThm1\. This contrast shows that usefulness is not always apparent from human inspection alone\.

These examples show that extracted theorems do not merely improve aggregate evaluation metrics, but also play concrete roles in individual proof constructions\. In particular, not only human\-interpretable theorems such asThm1andThm3, but also theorems whose usefulness is not obvious at first glance, such asThm2,Thm4, andThm5, function as effective supporting knowledge when an LLM constructs Hilbert\-system proofs\. More broadly, this suggests that theorem discovery without human prior knowledge may allow AI systems to surface useful lemmas that humans did not explicitly provide\.

## 6Related Work

#### Learning\-guided formal theorem proving\.

Prior work on learning\-guided formal theorem proving has studied reinforcement\-learning proof search, tactic prediction, proof generation, and LLM\-based proving in Lean\(Kaliszyket al\.,[2018](https://arxiv.org/html/2606.28747#bib.bib24); Hanet al\.,[2022](https://arxiv.org/html/2606.28747#bib.bib20); Poluet al\.,[2023](https://arxiv.org/html/2606.28747#bib.bib21); Yanget al\.,[2023](https://arxiv.org/html/2606.28747#bib.bib23); Xinet al\.,[2024](https://arxiv.org/html/2606.28747#bib.bib44); Zimmeret al\.,[2025](https://arxiv.org/html/2606.28747#bib.bib45); Hubertet al\.,[2026](https://arxiv.org/html/2606.28747#bib.bib46)\)\. These methods build strong provers using existing formal libraries or proof data\. In contrast, we ask how far theorem discovery and reuse can go using only the three axioms and one inference rule of a Hilbert axiom system\.

#### Self\-play and intrinsic theorem discovery\.

Another line reduces dependence on human proof examples by learning proof\-search or conjecturing through self\-play or intrinsic motivation\(Wuet al\.,[2021](https://arxiv.org/html/2606.28747#bib.bib25); Lampleet al\.,[2022](https://arxiv.org/html/2606.28747#bib.bib26); Poesiaet al\.,[2024](https://arxiv.org/html/2606.28747#bib.bib49); Laurent and Platzer,[2022](https://arxiv.org/html/2606.28747#bib.bib30); Dong and Ma,[2025](https://arxiv.org/html/2606.28747#bib.bib50); Zhaoet al\.,[2025](https://arxiv.org/html/2606.28747#bib.bib53)\)\.Kasrielet al\.\([2025](https://arxiv.org/html/2606.28747#bib.bib51)\)is especially close because it discovers useful theorems from axioms, reuses them for further search, and evaluates external usefulness by asking an LLM judge whether they appear useful\. Complementing this direction, we ask whether self\-supervised theorem\-discovery methods can find theorems that not only appear useful, but also actually improve LLM\-based proof search when supplied as lemmas\.

#### Goal\-conditioned and hindsight learning\.

Our learning rule relates to Hindsight Experience Replay and goal\-conditioned supervised learning, which reuse reached states as goals\(Andrychowiczet al\.,[2017](https://arxiv.org/html/2606.28747#bib.bib28); Ghoshet al\.,[2021](https://arxiv.org/html/2606.28747#bib.bib27)\)\. In our setting, the reached objects are theorems, not environment states, and some are reused as both training goals and action primitives in subsequent stack\-machine decision processes\. Thus, a proof prefix reaching a formula becomes hindsight supervision for proving it\. This connects goal relabeling with theorem\-proving library learning\.

#### Lemma discovery and library learning\.

Lemma discovery and library learning are important directions for accelerating proof search\(Yanget al\.,[2023](https://arxiv.org/html/2606.28747#bib.bib23); Wanget al\.,[2024](https://arxiv.org/html/2606.28747#bib.bib43)\)\. In contrast to methods that rely on existing formal libraries, human\-provided lemmas, or LLM\-based proving pipelines, our agent discovers useful theorems through proof search using only the axioms and inference rule\.

#### Curry–Howard motivation\.

Our stack\-machine view is also motivated by the Curry–Howard correspondence, which relates propositions to types and proofs to programs\(Howard,[1980](https://arxiv.org/html/2606.28747#bib.bib18); Sørensen and Urzyczyn,[2006](https://arxiv.org/html/2606.28747#bib.bib19)\)\. There, implication resembles a function type andMPresembles function application\. This is not central to our claims, but explains why Hilbert proofs can be flattened into action sequences that push axioms or lemmas and compose them on a stack\. OurMPimplementation follows this intuition by unifying an implication antecedent with another stack formula, as in Hindley–Milner type inference\(Hindley,[1969](https://arxiv.org/html/2606.28747#bib.bib15); Milner,[1978](https://arxiv.org/html/2606.28747#bib.bib16); Damas and Milner,[1982](https://arxiv.org/html/2606.28747#bib.bib17)\)\.

## 7Conclusions

We studied whether useful theorems can be discovered within a formal axiomatic system using only its primitive rules\. We formulated Hilbert\-system propositional theorem proving as a stack\-machine decision process and proposed a learning algorithm that grows a theorem library through proof search\. The algorithm treats reached theorems as future proof goals and extracts useful theorems for reuse as lemmas\. Experiments show that the agent discovers many theorems over multiple generations in the Hilbert axiom system and finds proofs for a meaningful fraction of the human\-written benchmark problems\. We also demonstrate that the extracted theorems improve LLM proof performance when provided as prompt lemmas\.

A limitation of this study is that our experiments are conducted in a single axiom system\. However, the proposed framework is not specific to this axiom system and should be applicable to multiple axiom systems; evaluating this broader applicability is a natural next step\. Furthermore, it also remains an important direction for future work to test whether the same approach can scale to richer formal systems with broader applications, such as first\-order logic, set theory, and more general mathematical domains\.

While we have focused on Hilbert\-style propositional theorem proving, our experiments provide evidence that useful theorems can emerge from proof search without relying on human\-provided theorem libraries\. More broadly, these findings suggest a path toward self\-evolving AI systems for mathematics: systems that autonomously expand their formal knowledge through proof search while keeping each discovery formally verifiable\.

## Acknowledgements

This work was partially supported by JST Moonshot R&D Grant Number JPMJPS2011, CREST Grant Number JPMJCR2015 and Basic Research Grant \(Super AI\) of Institute for AI and Beyond of the University of Tokyo\. Kazuki Ota was supported by JST SPRING, Grant Number JPMJSP2108\. Takayuki Osa was supported by JSPS KAKENHI Grant Number JP25K03176\.

## References

- M\. Andrychowicz, F\. Wolski, A\. Ray, J\. Schneider, R\. Fong, P\. Welinder, B\. McGrew, J\. Tobin, P\. Abbeel, and W\. Zaremba \(2017\)Hindsight experience replay\.InAdvances in Neural Information Processing Systems,Vol\.30,pp\. 5048–5058\.Cited by:[§4\.1](https://arxiv.org/html/2606.28747#S4.SS1.p7.1),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px3.p1.1)\.
- Z\. Azerbayev, H\. Schoelkopf, K\. Paster, M\. Dos Santos, S\. McAleer, A\. Q\. Jiang, J\. Deng, S\. Biderman, and S\. Welleck \(2024\)Llemma: an open language model for mathematics\.InInternational Conference on Learning Representations,Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p3.1)\.
- A\. Church \(1996\)Introduction to mathematical logic\.Princeton University Press,Princeton, NJ\.Note:Reprint of the revised 1956 edition\. See Propositions 235 and 239, pp\. 127–128Cited by:[§2](https://arxiv.org/html/2606.28747#S2.SS0.SSS0.Px3.p1.1)\.
- S\. A\. Cook and R\. A\. Reckhow \(1979\)The relative efficiency of propositional proof systems\.Journal of Symbolic Logic44\(1\),pp\. 36–50\.Cited by:[§2](https://arxiv.org/html/2606.28747#S2.SS0.SSS0.Px4.p1.1)\.
- S\. A\. Cook \(1971\)The complexity of theorem\-proving procedures\.InProceedings of the Third Annual ACM Symposium on Theory of Computing,pp\. 151–158\.Cited by:[§2](https://arxiv.org/html/2606.28747#S2.SS0.SSS0.Px4.p1.1)\.
- L\. Damas and R\. Milner \(1982\)Principal type\-schemes for functional programs\.InProceedings of the 9th ACM SIGPLAN\-SIGACT Symposium on Principles of Programming Languages,pp\. 207–212\.Cited by:[§3](https://arxiv.org/html/2606.28747#S3.p2.11),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px5.p1.1)\.
- K\. Dong and T\. Ma \(2025\)STP: self\-play LLM theorem provers with iterative conjecturing and proving\.InProceedings of the 42nd International Conference on Machine Learning,Proceedings of Machine Learning Research, Vol\.267,pp\. 14114–14136\.Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p2.1),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px2.p1.1)\.
- S\. Farquhar, J\. Kossen, L\. Kuhn, and Y\. Gal \(2024\)Detecting hallucinations in large language models using semantic entropy\.Nature630,pp\. 625–630\.External Links:[Document](https://dx.doi.org/10.1038/s41586-024-07421-0)Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p2.1)\.
- Gemini Team \(2025\)Gemini 2\.5: pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities\.Note:arXiv preprint arXiv:2507\.06261External Links:2507\.06261Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p1.1)\.
- D\. Ghosh, A\. Gupta, A\. Reddy, J\. Fu, C\. Devin, B\. Eysenbach, and S\. Levine \(2021\)Learning to reach goals via iterated supervised learning\.InInternational Conference on Learning Representations,Cited by:[§4\.1](https://arxiv.org/html/2606.28747#S4.SS1.p7.1),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px3.p1.1)\.
- J\. M\. Han, J\. Rute, Y\. Wu, E\. W\. Ayers, and S\. Polu \(2022\)Proof artifact co\-training for theorem proving with language models\.InInternational Conference on Learning Representations,Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p2.1),[§1](https://arxiv.org/html/2606.28747#S1.p3.1),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px1.p1.1)\.
- D\. Hilbert and W\. Ackermann \(1950\)Principles of mathematical logic\.Chelsea Publishing Company,New York\.Note:Translated by Lewis M\. Hammond, George G\. Leckie, and F\. SteinhardtCited by:[§2](https://arxiv.org/html/2606.28747#S2.SS0.SSS0.Px2.p1.5)\.
- R\. Hindley \(1969\)The principal type\-scheme of an object in combinatory logic\.Transactions of the American Mathematical Society146,pp\. 29–60\.Cited by:[§3](https://arxiv.org/html/2606.28747#S3.p2.11),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px5.p1.1)\.
- W\. A\. Howard \(1980\)The formulae\-as\-types notion of construction\.InTo H\. B\. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism,J\. P\. Seldin and J\. R\. Hindley \(Eds\.\),pp\. 479–490\.Cited by:[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px5.p1.1)\.
- T\. Hubert, R\. Mehta, L\. Sartran, M\. Z\. Horvath, G\. Zuzic, E\. Wieser, A\. Huang, J\. Schrittwieser, Y\. Schroecker, H\. Masoom, O\. Bertolli, T\. Zahavy, A\. Mandhane, J\. Yung, I\. Beloshapka, B\. Ibarz, V\. Veeriah, L\. Yu, O\. Nash, P\. Lezeau, S\. Mercuri, C\. Sonne, B\. Mehta, A\. Davies, D\. Zheng, F\. Pedregosa, Y\. Li, I\. von Glehn, M\. Rowland, S\. Albanie, A\. Velingker, S\. Schmitt, E\. Lockhart, E\. Hughes, H\. Michalewski, N\. Sonnerat, D\. Hassabis, P\. Kohli, and D\. Silver \(2026\)Olympiad\-level formal mathematical reasoning with reinforcement learning\.Nature651\(8106\),pp\. 607–613\.External Links:[Document](https://dx.doi.org/10.1038/s41586-025-09833-y)Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p2.1),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px1.p1.1)\.
- A\. Q\. Jiang, S\. Welleck, J\. P\. Zhou, T\. Lacroix, J\. Liu, W\. Li, M\. Jamnik, G\. Lample, and Y\. Wu \(2023\)Draft, sketch, and prove: guiding formal theorem provers with informal proofs\.InInternational Conference on Learning Representations,Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p2.1),[§1](https://arxiv.org/html/2606.28747#S1.p3.1)\.
- A\. T\. Kalai, O\. Nachum, S\. S\. Vempala, and E\. Zhang \(2025\)Why language models hallucinate\.Note:arXiv preprint arXiv:2509\.04664Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p2.1)\.
- C\. Kaliszyk, J\. Urban, H\. Michalewski, and M\. Olšák \(2018\)Reinforcement learning of theorem proving\.InAdvances in Neural Information Processing Systems,Vol\.31\.Cited by:[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px1.p1.1)\.
- T\. Kasriel, T\. Lu, Q\. Ding, J\. He, and D\. Song \(2025\)Usefulness\-driven learning of formal mathematics\.InThe 5th Workshop on Mathematical Reasoning and AI \(MATH\-AI\) at NeurIPS,Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p4.1),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px2.p1.1)\.
- S\. C\. Kleene \(1952\)Introduction to metamathematics\.Van Nostrand\.Cited by:[§5\.1](https://arxiv.org/html/2606.28747#S5.SS1.p2.2)\.
- G\. Lample, M\. Lachaux, T\. Lavril, X\. Martinet, A\. Hayat, G\. Ebner, A\. Rodriguez, and T\. Lacroix \(2022\)HyperTree proof search for neural theorem proving\.InAdvances in Neural Information Processing Systems,Vol\.35\.Cited by:[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px2.p1.1)\.
- J\. Laurent and A\. Platzer \(2022\)Learning to find proofs and theorems by learning to refine search strategies: the case of loop invariant synthesis\.InAdvances in Neural Information Processing Systems,Vol\.35,pp\. 4843–4856\.Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p4.1),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px2.p1.1)\.
- T\. Luong and E\. Lockhart \(2025\)Advanced version of Gemini with Deep Think officially achieves gold\-medal standard at the International Mathematical Olympiad\.Note:Google DeepMind blogURL:[https://deepmind\.google/blog/advanced\-version\-of\-gemini\-with\-deep\-think\-officially\-achieves\-gold\-medal\-standard\-at\-the\-international\-mathematical\-olympiad/](https://deepmind.google/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/)\. Accessed: May 25, 2026Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p1.1)\.
- E\. Mendelson \(2015\)Introduction to mathematical logic\.6 edition,CRC Press,Boca Raton\.External Links:ISBN 9781482237726Cited by:[§2](https://arxiv.org/html/2606.28747#S2.SS0.SSS0.Px2.p1.5)\.
- R\. Milner \(1978\)A theory of type polymorphism in programming\.Journal of Computer and System Sciences17\(3\),pp\. 348–375\.Cited by:[§3](https://arxiv.org/html/2606.28747#S3.p2.11),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px5.p1.1)\.
- OpenAI \(2023\)Introducing APIs for GPT\-3\.5 Turbo and Whisper\.Note:OpenAI blog\. URL:[https://openai\.com/index/introducing\-chatgpt\-and\-whisper\-apis/](https://openai.com/index/introducing-chatgpt-and-whisper-apis/)\. Accessed: May 25, 2026Cited by:[§5\.2](https://arxiv.org/html/2606.28747#S5.SS2.p4.1)\.
- OpenAI \(2024a\)GPT\-4o system card\.Note:URL:[https://openai\.com/index/gpt\-4o\-system\-card/](https://openai.com/index/gpt-4o-system-card/)\. Accessed: May 25, 2026Cited by:[§5\.2](https://arxiv.org/html/2606.28747#S5.SS2.p4.1)\.
- OpenAI \(2024b\)OpenAI o1 system card\.Note:URL:[https://openai\.com/index/openai\-o1\-system\-card/](https://openai.com/index/openai-o1-system-card/)\. Accessed: May 25, 2026External Links:2412\.16720Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p1.1)\.
- OpenAI \(2025\)GPT\-5 system card\.Note:URL:[https://openai\.com/index/gpt\-5\-system\-card/](https://openai.com/index/gpt-5-system-card/)\. Accessed: May 25, 2026Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p1.1),[§5\.2](https://arxiv.org/html/2606.28747#S5.SS2.p4.1)\.
- G\. Poesia, D\. Broman, N\. Haber, and N\. D\. Goodman \(2024\)Learning formal mathematics from intrinsic motivation\.InAdvances in Neural Information Processing Systems,Vol\.37\.Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p4.1),[§5\.1](https://arxiv.org/html/2606.28747#S5.SS1.p2.2),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px2.p1.1)\.
- S\. Polu, J\. M\. Han, K\. Zheng, M\. Baksys, I\. Babuschkin, and I\. Sutskever \(2023\)Formal mathematics statement curriculum learning\.InInternational Conference on Learning Representations,Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p2.1),[§1](https://arxiv.org/html/2606.28747#S1.p3.1),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px1.p1.1)\.
- E\. L\. Post \(1921\)Introduction to a general theory of elementary propositions\.American Journal of Mathematics43\(3\),pp\. 163–185\.Cited by:[§2](https://arxiv.org/html/2606.28747#S2.SS0.SSS0.Px1.p1.14)\.
- M\. H\. Sørensen and P\. Urzyczyn \(2006\)Lectures on the curry–howard isomorphism\.Studies in Logic and the Foundations of Mathematics, Vol\.149,Elsevier\.External Links:ISBN 9780444520777Cited by:[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px5.p1.1)\.
- T\. H\. Trinh, Y\. Wu, Q\. V\. Le, H\. He, and T\. Luong \(2024\)Solving olympiad geometry without human demonstrations\.Nature625,pp\. 476–482\.External Links:[Document](https://dx.doi.org/10.1038/s41586-023-06747-5)Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p2.1)\.
- H\. Wang, H\. Xin, C\. Zheng, Z\. Liu, Q\. Cao, Y\. Huang, J\. Xiong, H\. Shi, E\. Xie, J\. Yin, Z\. Li, and X\. Liang \(2024\)LEGO\-Prover: neural theorem proving with growing libraries\.InInternational Conference on Learning Representations,Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p2.1),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px4.p1.1)\.
- M\. Wu, M\. Norrish, C\. Walder, and A\. Dezfouli \(2021\)TacticZero: learning to prove theorems from scratch with deep reinforcement learning\.InAdvances in Neural Information Processing Systems,Vol\.34\.Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p4.1),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px2.p1.1)\.
- Y\. Wu, A\. Q\. Jiang, W\. Li, M\. N\. Rabe, C\. Staats, M\. Jamnik, and C\. Szegedy \(2022\)Autoformalization with large language models\.InAdvances in Neural Information Processing Systems,Vol\.35\.Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p2.1),[§1](https://arxiv.org/html/2606.28747#S1.p3.1)\.
- H\. Xin, D\. Guo, Z\. Shao, Z\. Ren, Q\. Zhu, B\. Liu, C\. Ruan, W\. Li, and X\. Liang \(2024\)DeepSeek\-Prover: advancing theorem proving in LLMs through large\-scale synthetic data\.Note:arXiv preprint arXiv:2405\.14333External Links:2405\.14333,[Document](https://dx.doi.org/10.48550/arXiv.2405.14333)Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p2.1),[§1](https://arxiv.org/html/2606.28747#S1.p3.1),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px1.p1.1)\.
- K\. Yang, A\. M\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. Anandkumar \(2023\)LeanDojo: theorem proving with retrieval\-augmented language models\.InAdvances in Neural Information Processing Systems,Vol\.36\.Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p2.1),[§1](https://arxiv.org/html/2606.28747#S1.p3.1),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px1.p1.1),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px4.p1.1)\.
- A\. Zhao, Y\. Wu, Y\. Yue, T\. Wu, Q\. Xu, Y\. Yue, M\. Lin, S\. Wang, Q\. Wu, Z\. Zheng, and G\. Huang \(2025\)Absolute zero: reinforced self\-play reasoning with zero data\.InAdvances in Neural Information Processing Systems,Vol\.38\.Cited by:[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px2.p1.1)\.
- M\. Zimmer, X\. Ji, R\. Tutunov, A\. Bordg, J\. Wang, and H\. Bou Ammar \(2025\)Bourbaki: self\-generated and goal\-conditioned MDPs for theorem proving\.Note:arXiv preprint arXiv:2507\.02726External Links:2507\.02726,[Document](https://dx.doi.org/10.48550/arXiv.2507.02726)Cited by:[§1](https://arxiv.org/html/2606.28747#S1.p2.1),[§6](https://arxiv.org/html/2606.28747#S6.SS0.SSS0.Px1.p1.1)\.

## Appendix AExperimental Details

In this section, we explain implementation details for theorem\-discovery training and library construction\. Each generation uses2525training iterations\. In each iteration, the agent generates81928192episodes, and each episode has a maximum length of77steps\. Therefore, each generation uses25×8192×725\\times 8192\\times 7simulator evaluations\. Episodes are processed in batches of20482048episodes\.

The policy is parameterized by a Transformer network\. The model uses embedding dimension128128, four Transformer blocks, four attention heads, feed\-forward dimension512512, dropout rate0\.10\.1, and learned positional encodings\. The policy is trained with cross\-entropy loss under a legal\-action mask\. We use Adam with learning rate0\.0010\.001, batch size512512, and one training epoch per iteration\.

The policy observation is a fixed\-length sequence of10241024integer tokens\. It consists of the sampled goal formula followed by the current proof stack, separated by a special field\-separator token, and padded to a fixed length\. Each formula is tokenized at the symbol level in reverse Polish notation, with tokens for implication, falsity, variables, and formula separators\. Thus, a training example forπθ​\(A\|S,g\)\\pi\_\{\\theta\}\(A\|S,g\)presents the goal formulaggand the current stackSSto the Transformer\.

Across generations, the action space consists of the three axiom actions, theMPaction, and the library theorem actions available at that generation\. The legal\-action mask is computed from the current stack, the remaining horizon, and the current action space\. It is used to mask illegal actions during sampling and in the cross\-entropy loss\. When new theorems are extracted and added to the library, the action space changes accordingly\. We therefore initialize and train a new policy network for the updated action space at each generation\.

## Appendix BPrompts for LLM Evaluation

We show the prompt template used for LLM evaluation\. In the prompt, the axioms corresponding toAx1,Ax2, andAx3in the main text are denoted by ‘A01’, ‘A02’, and ‘A03’, respectively, and Modus Ponens is denoted by ‘MP’\. When discovered theorems are provided as lemmas, they are listed as ‘L01’, ‘L02’, and so on\. For the baseline without lemmas, this lemma list is empty, and the LLM is asked to construct a proof using only ‘A01’, ‘A02’, ‘A03’, and ‘MP’\. The final answer is requested as an RPN sequence in which actions are separated by spaces\.

\#Rules

ProvethegivenpropositionintheHilbertsystem\(withaxiomsA01,A02,A03andtheinferenceruleModusPonens\)\.

\#\#Axioms:

A01:A\-\>\(B\-\>A\)

A02:\(A\-\>\(B\-\>C\)\)\-\>\(\(A\-\>B\)\-\>\(A\-\>C\)\)

A03:\(\!A\-\>\!B\)\-\>\(B\-\>A\)

\#\#InferenceRule\(MP\):

Inthestack,thetopelementisregardedasX\-\>Y,andtheonebelowitasX\.UnifytheantecedentsofXandX\-\>YasinHindley\-Milnertypeinference,andasaresultderivetheconsequentY,whichisthenpushedontothestack\.Forexample,ifthetopofthestackis\(A\-\>\(B\-\>C\)\)\-\>\(\(A\-\>B\)\-\>\(A\-\>C\)\)andthenextoneisA\-\>\(B\-\>A\),thenA\-\>\(B\-\>C\)andA\-\>\(B\-\>A\)areunifiedwithA=C,yieldingtheresult\(A\-\>B\)\-\>\(A\-\>A\)\.

\#\#Lemmas:

Youcanusethefollowinglemmasifyouneed\.

L01:\(A\-\>B\)\-\>\(\(C\-\>A\)\-\>\(C\-\>B\)\)

L02:\(A\-\>\(B\-\>C\)\)\-\>\(B\-\>\(A\-\>C\)\)

\#OutputFormat

TheproofmustultimatelyberepresentedasacombinatorexpressioninReversePolishNotation\(RPN\)\.InRPN,A01,A02,A03eachpushaninstanceofthecorrespondingaxiomontothestack,L01,L02,\.\.\.dothesameforlemmas,andMPrepresentsModusPonensaccordingtotheaboverule\.Youmayincludeexplanations,butenclosethefinalproofexpressionbetween<final\_answer\>and</final\_answer\>\.

\#ExampleProblem

Targetproposition:A\-\>A

Referenceproofsteps:

1\.A\-\>\(B\-\>A\)\(AxiomA01\)

2\.A\-\>\(B\-\>A\)\(AxiomA01\)

3\.\(A\-\>\(B\-\>C\)\)\-\>\(\(A\-\>B\)\-\>\(A\-\>C\)\)\(AxiomA02\)

4\.\(A\-\>B\)\-\>\(A\-\>A\)\(ApplyMPto3and2\)

5\.A\-\>A\(ApplyMPto4and1\)

Inthiscase,thecombinatorexpressioninRPNisA01A01A02MPMP\.Finaloutputexampleisthefollowing:

<final\_answer\>A01A01A02MPMP</final\_answer\>

\#Problem

Provethefollowingproposition:

\(A\-\>B\)\-\>\(\(B\-\>C\)\-\>\(A\-\>C\)\)