# Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving

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

## Key facts

- Cited by 12 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 7 of its 16 references that are in the map.
- First posted on arXiv 3 Jul 2025.

## 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, 7 of 7)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [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: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4](https://mlsanity.com/paper/2410.16429/) (2024)

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

- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Scalable Power Sampling: Unlocking Efficient, Training-Free Reasoning for LLMs via Distribution Sharpening](https://mlsanity.com/paper/2601.21590/) (2026)
- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [OProver: A Unified Framework for Agentic Formal Theorem Proving](https://mlsanity.com/paper/2605.17283/) (2026)
- [The Y-Combinator for LLMs: Solving Long-Context Rot with λ-Calculus](https://mlsanity.com/paper/2603.20105/) (2026)
- [Decoding as Optimisation on the Probability Simplex: From Top-K to Top-P (Nucleus) to Best-of-K Samplers](https://mlsanity.com/paper/2602.18292/) (2026)
- [Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models](https://mlsanity.com/paper/2602.10538/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [The Topological Dual of a Dataset: A Logic-to-Topology Encoding for AlphaGeometry-Style Data](https://mlsanity.com/paper/2604.18050/) (2026)
- [Self-Supervised Theorem Discovery in a Formal Axiomatic System](https://mlsanity.com/paper/2606.28747/) (2026)
- [iSDFT: Information-Proximal Self-Distillation for Continual Learning in LLMs](https://mlsanity.com/paper/2609.24646/) (2026)
- [A Critical Look at Power Sampling when Test Time Sharpening LLMs](https://mlsanity.com/paper/2610.13653/) (2026)

## Abstract (arXiv)

Reasoning remains a challenging task for large language models (LLMs), especially within the logically constrained environment of automated theorem proving (ATP), due to sparse rewards and the vast scale of proofs. These challenges are amplified in benchmarks like PutnamBench, which contains university-level problems requiring complex, multi-step reasoning. To address this, we introduce self-generated goal-conditioned MDPs (sG-MDPs), a new framework in which agents generate and pursue their subgoals based on the evolving proof state. Given this more structured generation of goals, the resulting problem becomes more amenable to search. We then apply Monte Carlo Tree Search (MCTS)-like algorithms to solve the sG-MDP, instantiating our approach in Bourbaki (7B), a modular system that can ensemble multiple 7B LLMs for subgoal generation and tactic synthesis. On PutnamBench, Bourbaki (7B) solves 26 problems, achieving new state-of-the-art results with models at this scale.