# A Theoretical Framework for Self-Play Theorem Proving Algorithms

arXiv: https://arxiv.org/abs/2606.01861 · HTML: https://mlsanity.com/paper/2606.01861/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Self-play RL for reasoning, one of 13 directions in Synthetic data and self-improvement for LLMs.
- Builds on 25 of its 44 references that are in the map.
- First posted on arXiv 1 Jun 2026.

## Placed in

- Synthetic data and self-improvement for LLMs / [Self-play RL for reasoning](https://mlsanity.com/synth/self-play-rl-for-reasoning/)

## Builds on (most cited first, 25 of 25)

- [A Simple Framework for Contrastive Learning of Visual Representations](https://mlsanity.com/paper/2002.05709/) (2020)
- [Representation Learning with Contrastive Predictive Coding](https://mlsanity.com/paper/1807.03748/) (2018)
- [Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm](https://mlsanity.com/paper/1712.01815/) (2017)
- [Wasserstein GAN](https://mlsanity.com/paper/1701.07875/) (2017)
- [Provable Guarantees for Self-Supervised Deep Learning with Spectral Contrastive Loss](https://mlsanity.com/paper/2106.04156/) (2021)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Near-Optimal Reinforcement Learning with Self-Play](https://mlsanity.com/paper/2006.12007/) (2020)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [Low-rank Solutions of Linear Matrix Equations via Procrustes Flow](https://mlsanity.com/paper/1507.03566/) (2015)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [Learning Formal Mathematics From Intrinsic Motivation](https://mlsanity.com/paper/2407.00695/) (2024)
- [Early science acceleration experiments with GPT-5](https://mlsanity.com/paper/2511.16072/) (2025)
- [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://mlsanity.com/paper/2507.15225/) (2025)
- [InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search](https://mlsanity.com/paper/2410.15700/) (2024)
- [Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers](https://mlsanity.com/paper/2509.06493/) (2025)
- [Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning](https://mlsanity.com/paper/2507.08649/) (2025)
- [Metastable Dynamics of Chain-of-Thought Reasoning: Provable Benefits of Search, RL and Distillation](https://mlsanity.com/paper/2502.01694/) (2025)
- [StepFun-Prover Preview: Let's Think and Verify Step by Step](https://mlsanity.com/paper/2507.20199/) (2025)
- [On Learning Verifiers and Implications to Chain-of-Thought Reasoning](https://mlsanity.com/paper/2505.22650/) (2025)
- [Artificial Intelligence and the Structure of Mathematics](https://mlsanity.com/paper/2604.06107/) (2026)

## Built on by (most cited first, 1 of 1)

- [Recursive Self-Improvement in AI: From Bounded Self-Refinement to Autonomous Research Loops](https://mlsanity.com/paper/2607.07663/) (2026)

## Abstract (arXiv)

Self-play, a type of training algorithm that enables a model to self-improve, has recently shown promising empirical results in the context of formal theorem proving using Large Language Models (LLMs). (Dong & Ma, 2025) instantiate self-play with two cooperating agents: a prover, which proves theorems, and a conjecturer, which generates new theorems as a curriculum to the prover. In this paper, we provide a theoretical framework for understanding the self-improvement capabilities of self-play algorithms for theorem proving. First, we formalize the set of theorems as a graph, with nodes as theorems and edges between pairs of theorems with similar semantics. We introduce a set of primitive assumptions that characterize the guarantees of a trained prover and how a conjecturer can access the structure of the graph. Second, we show that if the underlying graph of theorems is well-connected, then a prover-conjecturer system, where the conjecturing algorithm is based on a reversible random walk, is sufficient to grow the set of proved theorems exponentially. Third, motivated by an issue encountered empirically by self-play algorithms, where the conjecturer tends to generate artificially complex and non-fundamental theorems, we propose a diversity measure for a training distribution of theorems generated by a conjecturer and an improved conjecturing algorithm that locally maximizes this diversity measure, by computing the diffusion similarity between neighboring theorems in the theorem graph. Finally, we describe a method to compute the diffusion similarity by using contrastive learning to embed nodes into Euclidean space and then computing the inner-product between embeddings.