---
title: "Bourbaki — paper by Zimmer et al. (2025) — summary and ideas"
description: "They define self-generated goal-conditioned MDPs (sG-MDPs), where the agent invents its own… 16 references, cited by 5 papers here."
authors: ["Matthieu Zimmer", "Xiaotong Ji", "Rasul Tutunov", "Anthony Bordg", "Jun Wang", "Haitham Bou Ammar"]
year: 2025
venue: "arXiv:2507.02726"
source: "https://arxiv.org/abs/2507.02726"
doi: "10.48550/arxiv.2507.02726"
arxiv: "2507.02726"
licence: "CC BY 4.0 (arXiv)"
licence_url: "http://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/zimmer-2025-bourbaki-self-generated-goal-conditioned/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/zimmer-2025-bourbaki-self-generated-goal-conditioned/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2025](https://md.research.elamur.ai/free/en/papers/2025/page/13/) / Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving

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

**Authors:** Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov, Anthony Bordg, [Jun Wang](https://md.research.elamur.ai/free/en/authors/jun-wang/) and Haitham Bou Ammar · **Year:** 2025 · **Venue:** arXiv:2507.02726 · **Licence:** [CC BY 4.0 (arXiv)](http://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://arxiv.org/abs/2507.02726) · [PDF](https://arxiv.org/pdf/2507.02726) · [DOI 10.48550/arxiv.2507.02726](https://doi.org/10.48550/arxiv.2507.02726) · [arXiv 2507.02726](https://arxiv.org/abs/2507.02726) · [OpenAlex](https://openalex.org/W6891948351)

**Citations:** 0 citations (OpenAlex, 2026-10-14) · [5](https://md.research.elamur.ai/free/en/papers/zimmer-2025-bourbaki-self-generated-goal-conditioned/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Formal theorem proving is hard for LLMs because feedback is extremely sparse: a prover usually learns nothing until an entire Lean proof checks, and long proofs make blind search costly. This is especially limiting on PutnamBench, which formalises university-level Putnam competition problems. The authors draw on how mathematicians break a hard result into intermediate lemmas. They define self-generated goal-conditioned MDPs (sG-MDPs), where the agent invents its own subgoals during the proof, conditioned on what has already been established. In standard goal-conditioned RL, the goals are fixed in advance. Here, an LLM proposes subgoals as Lean statements, each of which must then be proven with Lean4 tactics. This gives the search intermediate signals of progress. The resulting MDP is solved with MCTS-style search, though RL training is also possible. Their system, Bourbaki (7B), combines several 7B provers for subgoal proposal and tactic generation. It reaches a new state of the art for this model size on PutnamBench. This suggests that structured subgoal search can partly offset small model scale.

## Key points
- Bourbaki (7B) ensembles DeepSeek-Prover-v2–7B and Kimina-7B, and its modular design lets other models be added.
- On PutnamBench it proves 26 problems, compared with 10 for the previous best 7B entry on the official leaderboard (Kimina-7B).
- It also beats InternLM2.5-StepProver, DeepSeek-Prover-v2 7B (with and without CoT), Goedel-Prover, STP and ABEL at the 7B scale.
- It is sample-efficient at small budgets:
  - With a 128-sample budget on DeepSeek-Prover-v2 (non-CoT), it solves 23/658 problems versus 15/658 for the base model.
  - On STP, it solves 7/644 versus 6/644 at 64 samples, and 8/644 versus 7/644 at 128 samples.
- For context, the much larger DeepSeek-Prover-V2 (>100B parameters) solves 49/658 PutnamBench problems.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

📚 Shelves (2): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov, Anthony Bordg, Jun Wang and Haitham Bou Ammar. 2025. Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving. arXiv:2507.02726.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{zimmer2025bourbaki,
  title = {{Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving}},
  author = {Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov, Anthony Bordg, Jun Wang and Haitham Bou Ammar},
  year = {2025},
  doi = {10.48550/arxiv.2507.02726},
  eprint = {2507.02726},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2507.02726}
}
```

- [← previous BiMediX2 : Bio-Medical EXpert LMM for Diverse Medical Modalities](https://md.research.elamur.ai/free/en/papers/mullappilly-2025-bimedix2-bio-medical-expert-lmm/)
- [next → Conflicting Needles in a Haystack: How LLMs behave when faced with contradictory information](https://md.research.elamur.ai/free/en/papers/kurfali-2025-conflicting-needles-haystack-how-llms/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/13/)

## References

16 references, 11 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. AlphaGeometry Team AlphaProof. Ai achieves silver-medal standard solving international mathematical olympiad problems. 2024. URL [https://deepmind.google/discover/](https://deepmind.google/discover/) blog/ai-solves-imo-problems-at-silver-medal-level/. [↗](https://deepmind.google/discover/)
2. Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, and Sanmi Koyejo. [Pantograph: A machine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4](https://md.research.elamur.ai/free/en/papers/aniva-2024-pantograph-machine-machine-interaction-interface/). In International Conference on Tools and Algorithms for the Construction and Analysis of…
3. Kefan Dong and Tengyu Ma. [Stp: Self-play llm theorem provers with iterative conjecturing and proving](https://md.research.elamur.ai/free/en/papers/dong-2025-stp-self-play-llm-theorem/). arXiv e-prints, pp. arXiv–2502, 2025.
4. Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve, and Amaury Hayat. Abel: Sample efficient online reinforcement learning for neural theorem proving. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24, 2024. [find](https://scholar.google.com/scholar?q=Fabian+Gloeckle%2C+Jannis+Limperg%2C+Gabriel+Synnaeve%2C+and+Amaury+Hayat%2E+Abel%3A+Sample+efficient+online+reinforcement+learning+for+neural+theorem+proving%2E+In+The+4th+Workshop+on+Mathematical+Reasoning+and+)
5. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. [Proof artifact co-training for theorem proving with language models](https://md.research.elamur.ai/free/en/papers/han-2021-proof-artifact-co-training-theorem/), 2022. URL [https://arxiv.org/](https://arxiv.org/) abs/2102.06203. [↗](https://arxiv.org/)
6. Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. [Hypertree proof search for neural theorem proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/), 2022. URL https://arxiv.org/abs/2205.11491. [↗](https://arxiv.org/abs/2205.11491)
7. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. [Goedel-prover: A frontier model for open-source automated theorem proving](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/). arXiv preprint arXiv:2502.07640, 2025.
8. Minghuan Liu, Menghui Zhu, and Weinan Zhang. Goal-conditioned reinforcement learning: Problems and solutions, 2022. URL https://arxiv.org/abs/2201.08299. — [arXiv:2201.08299](https://arxiv.org/abs/2201.08299) [↗](https://arxiv.org/abs/2201.08299)
9. ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. [Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition](https://md.research.elamur.ai/free/en/papers/ren-2025-deepseek-prover-v2-advancing-formal/). arXiv preprint arXiv:2504.21801, 2025.
10. Tom Schaul, Daniel Horgan, Karol Gregor, and David Silver. Universal value function approximators. In Francis Bach and David Blei (eds.), Proceedings of the 32nd International Conference on Machine Learning, volume 37 of Proceedings of Machine Learning Research, pp. 1312–1320, Lille, France, 07–09 J… [find](https://scholar.google.com/scholar?q=Tom+Schaul%2C+Daniel+Horgan%2C+Karol+Gregor%2C+and+David+Silver%2E+Universal+value+function+approximators%2E+In+Francis+Bach+and+David+Blei+%28eds%2E%29%2C+Proceedings+of+the+32nd+International+Conference+on+Machine+Le)
11. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: A multilingual competition-mathematics benchmark for formal theorem-proving. In AI for Math Workshop@ ICML 2024, 2024. [find](https://scholar.google.com/scholar?q=George+Tsoukalas%2C+Jasper+Lee%2C+John+Jennings%2C+Jimmy+Xin%2C+Michelle+Ding%2C+Michael+Jennings%2C+Amitayush+Thakur%2C+and+Swarat+Chaudhuri%2E+Putnambench%3A+A+multilingual+competition%2Dmathematics+benchmark+for+forma)
12. Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li, and Xiaodan Liang. [DT-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function](https://md.research.elamur.ai/free/en/papers/wang-2023-dt-solver-automated-theorem-proving/). In Anna Rogers, Jordan Boyd-Graber, and Naoa…
13. Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. [Kimina-prover preview: Towards large formal reasoning models with reinforcement learning](https://md.research.elamur.ai/free/en/papers/wang-2025-kimina-prover-preview-large-formal/). arXiv preprint arXiv:2504.11354, 2025.
14. Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.[15700, 2024](https://md.research.elamur.ai/free/en/papers/wu-2024-internlm2-5-stepprover-advancing-automated/).
15. Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-… — [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-v1-5-harnessing/)
16. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. [Leandojo: Theorem proving with retrieval-augmented language models](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/). Advances in Neural Information Processing Systems, 36:21573– 21612, 2023.

*Updated 3 November 2026*