Elamur Research⌕
☰
home / papers / 2025 / Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving

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

Paper · 2025 · Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov et al.

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.

 Fields, topics and concepts

📚 Shelves 2The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 works

🧭 Topics 1Research subjects and languages the work is about.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. DOI 10.48550/arxiv.2507.02726 · arXiv 2507.02726

@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}
}

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/ blog/ai-solves-imo-problems-at-silver-medal-level/. ↗
  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. 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. 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
  5. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models, 2022. URL https://arxiv.org/ abs/2102.06203. ↗
  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, 2022. URL 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. 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) ↗
  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. 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
  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
  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. 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. 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.
  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
  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. Advances in Neural Information Processing Systems, 36:21573– 21612, 2023.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/zimmer-2025-bourbaki-self-generated-goal-conditioned/