---
title: "Leanabell-Prover: Posttraining Scaling in Formal Reasoning (2025)"
description: "Reasoning models such as OpenAI O1/O3 and Deepseek R1 have gained a lot from posttraining… 39 references, cited by 21 papers here."
authors: ["Jingyuan Zhang", "Qi Wang", "Xingguang Ji", "Yahui Liu", "Yang Yue", "Fuzheng Zhang", "Di Zhang", "Guorui Zhou", "Kun Gai"]
year: 2025
venue: "arXiv:2504.06122"
source: "https://arxiv.org/abs/2504.06122"
doi: "10.48550/arxiv.2504.06122"
arxiv: "2504.06122"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/zhang-2025-leanabell-prover-posttraining-scaling-formal/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/zhang-2025-leanabell-prover-posttraining-scaling-formal/)

[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/6/) / Leanabell-Prover: Posttraining Scaling in Formal Reasoning

# Leanabell-Prover: Posttraining Scaling in Formal Reasoning

**Authors:** [Jingyuan Zhang](https://md.research.elamur.ai/free/en/authors/jingyuan-zhang/), Qi Wang, Xingguang Ji, [Yahui Liu](https://md.research.elamur.ai/free/en/authors/yahui-liu/), [Yang Yue](https://md.research.elamur.ai/free/en/authors/yang-yue/), [Fuzheng Zhang](https://md.research.elamur.ai/free/en/authors/fuzheng-zhang/), [Di Zhang](https://md.research.elamur.ai/free/en/authors/di-zhang/), [Guorui Zhou](https://md.research.elamur.ai/free/en/authors/guorui-zhou/) and [Kun Gai](https://md.research.elamur.ai/free/en/authors/kun-gai/) · **Year:** 2025 · **Venue:** arXiv:2504.06122 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

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

**Citations:** 0 citations (OpenAlex, 2026-10-14) · [21](https://md.research.elamur.ai/free/en/papers/zhang-2025-leanabell-prover-posttraining-scaling-formal/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Reasoning models such as OpenAI O1/O3 and Deepseek R1 have gained a lot from posttraining scaling. Automated theorem proving (ATP) in Lean 4 has seen little of that benefit so far. This work, from Kuaishou Technology, asks whether the same recipe helps provers that write a complete proof in one pass.

The authors start from two 7B models, DeepSeek-Prover-v1.5-SFT and Goedel-Prover-SFT, and apply two further training phases:
- **Continual training** on a large mixed corpus of formal statements and verified proofs, supplemented with synthetic chain-of-thought data. This data is meant to teach behaviours like checking one's own work and dropping failing approaches.
- **Reinforcement learning** with GRPO, where the only reward is whether the Lean 4 compiler accepts the proof.

Both base models improve, and the stronger variant reaches 59.8% pass@32 on MiniF2F-test, a state-of-the-art result for whole-proof generation. The work matters because it shows RL can push formal provers further. It also reveals real limits: the base models are weak, and the reflective behaviours fade during RL.

## Key points
- **Training corpus:** about 1.52M formal statements, of which 0.22M also carry informal comments and verified proofs.
  - Sources are Lean Workbook, STP-Lean, NuminaMath (520K), AoPS (370K) and PromptCoT (90K).
  - Natural-language problems were converted by a formalizer built on Qwen2.5-32B-Coder-Instruct.
- **RL setup:** reinforcement learning from proof assistant feedback (RLPAF) using GRPO, with Lean 4 verification as a binary outcome reward.
- **Results on MiniF2F-test (pass@32):**
  - Leanabell-Prover-DS-RL scores 56.6%, versus 50.0% for DeepSeek-Prover-v1.5-RL.
  - Leanabell-Prover-GD-RL scores 59.8%, versus 57.6% for Goedel-Prover-SFT; it rises to 61.1% at pass@128.
- **Comparison and limitations:**
  - Prompting Deepseek R1 directly for formal proofs gives only 51.6% pass@32.
  - Self-reflection abilities weaken after RL, and the choice of prompt set strongly affects RL gains.
- **Release:** data and intermediate models are published at github.com/Leanabell-LM/Leanabell-Prover.

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

## Institutions

- [Kuaishou](https://md.research.elamur.ai/free/en/companies/kuaishou/) — Company, Beijing, China · 20 works · 116 citations

📚 Shelves (3): [🖥️ 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 · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

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

## Cite

Cite as: Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou and Kun Gai. 2025. Leanabell-Prover: Posttraining Scaling in Formal Reasoning. arXiv:2504.06122.

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

```bibtex
@misc{zhang2025leanabell,
  title = {{Leanabell-Prover: Posttraining Scaling in Formal Reasoning}},
  author = {Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou and Kun Gai},
  year = {2025},
  doi = {10.48550/arxiv.2504.06122},
  eprint = {2504.06122},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2504.06122}
}
```

- [← previous KITAB-Bench: A Comprehensive Multi-Domain Benchmark for Arabic OCR and Document Understanding](https://md.research.elamur.ai/free/en/papers/heakl-2025-kitab-bench-comprehensive-multi-domain/)
- [next → LongReward: Improving Long-context Large Language Models with AI Feedback](https://md.research.elamur.ai/free/en/papers/zhang-2025-longreward-improving-long-context-large/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/6/)

## References

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

1. Anthropic. Claude 3.7 Sonnet System card. 2025. URL [https://www.anthropic.com/news/claude-3-7-sonnet](https://www.anthropic.com/news/claude-3-7-sonnet) . [↗](https://www.anthropic.com/news/claude-3-7-sonnet)
2. AoPS. Art of problem solving. [https://artofproblemsolving.com/](https://artofproblemsolving.com/) . Accessed: [date]. [↗](https://artofproblemsolving.com/)
3. Z. Azerbayev, H. Schoelkopf, K. Paster, M. D. Santos, S. McAleer, A. Q. Jiang, J. Deng, S. Biderman, and S. Welleck. [Llemma: An open language model for mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-llemma-open-language-model-mathematics/). arXiv preprint arXiv:2310.10631, 2023.
4. R. Coulom. Efficient selectivity and backup operators in monte-carlo tree search. In International conference on computers and games, pages 72–83. Springer, 2006. [find](https://scholar.google.com/scholar?q=R%2E+Coulom%2E+Efficient+selectivity+and+backup+operators+in+monte%2Dcarlo+tree+search%2E+In+International+conference+on+computers+and+games%2C+pages+72%E2%80%9383%2E+Springer%2C+2006%2E)
5. L. De Moura, S. Kong, J. Avigad, F. Van Doorn, and J. von Raumer. The Lean theorem prover (system description). In International Conference on Automated Deduction (CAD), 2015. [find](https://scholar.google.com/scholar?q=L%2E+De+Moura%2C+S%2E+Kong%2C+J%2E+Avigad%2C+F%2E+Van+Doorn%2C+and+J%2E+von+Raumer%2E+The+Lean+theorem+prover+%28system+description%29%2E+In+International+Conference+on+Automated+Deduction+%28CAD%29%2C+2015%2E)
6. DeepMind. Alphaproof and Alphageometry, July 2024. URL [https://deepmind.googl](https://deepmind.googl) e/discover/blog/ai-solves-imo-problems-at-silver-medal-level/ . [↗](https://deepmind.googl)
7. K. Dong and T. 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 preprint arXiv:2502.00212, 2025.
8. K. Gandhi, A. Chakravarthy, A. Singh, N. Lile, and N. D. Goodman. [Cognitive behaviors that enable self-improving reasoners, or, four habits of highly effective stars](https://md.research.elamur.ai/free/en/papers/gandhi-2025-cognitive-behaviors-that-enable-self/). arXiv preprint arXiv:2503.01307, 2025.
9. D. Guo, D. Yang, H. Zhang, J. Song, R. Zhang, R. Xu, Q. Zhu, S. Ma, P. Wang, X. Bi, et al. [Deepseek-R1: Incentivizing reasoning capability in llms via reinforcement learning](https://md.research.elamur.ai/free/en/papers/deepseek-ai-2025-deepseek-r1-incentivizing-reasoning-capability/). arXiv preprint arXiv:2501.12948, 2025.
10. B. Hui, J. Yang, Z. Cui, J. Yang, D. Liu, L. Zhang, T. Liu, J. Zhang, B. Yu, K. Dang, et al. Qwen2. 5-coder technical report. arXiv preprint arXiv:2409.[12186, 2024](https://md.research.elamur.ai/free/en/papers/hui-2024-qwen2-5-coder-technical-report/).
11. G. Lample, T. Lacroix, M.-A. Lachaux, A. Rodriguez, A. Hayat, T. Lavril, G. Ebner, and X. Martinet. [Hypertree proof search for neural theorem proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/). Advances in Neural Information Processing Systems (NeurIPS), 35, 2022.
12. J. Li, E. Beeching, L. Tunstall, B. Lipkin, R. Soletskyi, S. C. Huang, K. Rasul, L. Yu, A. Jiang, Z. Shen, Z. Qin, B. Dong, L. Zhou, Y. Fleureau, G. Lample, and S. Polu. Numinamath, 2024. [find](https://scholar.google.com/scholar?q=J%2E+Li%2C+E%2E+Beeching%2C+L%2E+Tunstall%2C+B%2E+Lipkin%2C+R%2E+Soletskyi%2C+S%2E+C%2E+Huang%2C+K%2E+Rasul%2C+L%2E+Yu%2C+A%2E+Jiang%2C+Z%2E+Shen%2C+Z%2E+Qin%2C+B%2E+Dong%2C+L%2E+Zhou%2C+Y%2E+Fleureau%2C+G%2E+Lample%2C+and+S%2E+Polu%2E+Numinamath%2C+2024%2E)
13. Y. Li, D. Du, L. Song, C. Li, W. Wang, T. Yang, and H. Mi. [Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving](https://md.research.elamur.ai/free/en/papers/li-2024-hunyuanprover-scalable-data-synthesis/). arXiv preprint arXiv:2412.20735, 2024.
14. H. Lin, Z. Sun, Y. Yang, and S. Welleck. [Lean-star: Learning to interleave thinking and proving](https://md.research.elamur.ai/free/en/papers/lin-2024-lean-star-learning-interleave-thinking/). arXiv preprint arXiv:2407.10040, 2024.
15. Y. Lin, S. Tang, B. Lyu, J. Wu, H. Lin, K. Yang, J. Li, M. Xia, D. Chen, S. 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.
16. Z. Liu, C. Chen, W. Li, P. Qi, T. Pang, C. Du, W. S. Lee, and M. Lin. [Understanding r1-zero-like training: A critical perspective](https://md.research.elamur.ai/free/en/papers/liu-2025-understanding-r1-zero-like-training/). arXiv preprint arXiv:2503.20783, 2025.
17. mathlib4. The math library of lean 4, 2025. URL [https://github.com/leanprover-c](https://github.com/leanprover-c) ommunity/mathlib4 . [↗](https://github.com/leanprover-c)
18. L. d. Moura and S. Ullrich. The lean 4 theorem prover and programming language. In International Conference on Automated Deduction, 2021. — [The Lean 4 Theorem Prover and Programming Language (System Description)](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/)
19. L. C. Paulson. Isabelle: A generic theorem prover. Springer, 1994. [find](https://scholar.google.com/scholar?q=L%2E+C%2E+Paulson%2E+Isabelle%3A+A+generic+theorem+prover%2E+Springer%2C+1994%2E)
20. S. Polu and I. Sutskever. [Generative language modeling for automated theorem proving](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/). arXiv preprint arXiv:2009.03393, 2020.
21. S. Polu, J. M. Han, K. Zheng, M. Baksys, I. Babuschkin, and I. Sutskever. [Formal mathematics statement curriculum learning](https://md.research.elamur.ai/free/en/papers/polu-2022-formal-mathematics-statement-curriculum-learning/). arXiv preprint arXiv:2202.01344, 2022.
22. R. Rafailov, A. Sharma, E. Mitchell, C. D. Manning, S. Ermon, and C. Finn. [Direct preference optimization: Your language model is secretly a reward model](https://md.research.elamur.ai/free/en/papers/rafailov-2023-direct-preference-optimization-language-model/). Advances in Neural Information Processing Systems (NeurIPS), 2023.
23. Z. Shao, P. Wang, Q. Zhu, R. Xu, J. Song, X. Bi, H. Zhang, M. Zhang, Y. Li, Y. Wu, et al. [Deepseekmath: Pushing the limits of mathematical reasoning in open language models](https://md.research.elamur.ai/free/en/papers/shao-2024-deepseekmath-pushing-limits-mathematical-reasoning/). arXiv preprint arXiv:2402.03300, 2024.
24. Q. Team. Qwen2.5: A party of foundation models, September 2024. URL https://qwen lm.github.io/blog/qwen2.5/ . [find](https://scholar.google.com/scholar?q=Q%2E+Team%2E+Qwen2%2E5%3A+A+party+of+foundation+models%2C+September+2024%2E+URL+https%3A%2F%2Fqwen+lm%2Egithub%2Eio%2Fblog%2Fqwen2%2E5%2F+%2E)
25. Q. Team. Qwq-32b: Embracing the power of reinforcement learning, March 2025. URL [https://qwenlm.github.io/blog/qwq-32b/](https://qwenlm.github.io/blog/qwq-32b/) . [↗](https://qwenlm.github.io/blog/qwq-32b/)
26. T. H. Trinh, Y. Wu, Q. V. Le, H. He, and T. Luong. [Solving olympiad geometry without human demonstrations](https://md.research.elamur.ai/free/en/papers/trinh-2024-solving-olympiad-geometry-without-human/). Nature, 625(7995):476–482, 2024.
27. Z. Wan, Y. Li, Y. Song, H. Wang, L. Yang, M. Schmidt, J. Wang, W. Zhang, S. Hu, and Y. Wen. Rema: Learning to meta-think for llms with multi-agent reinforcement learning. arXiv preprint arXiv:2503.09501, 2025. — [arXiv:2503.09501](https://arxiv.org/abs/2503.09501) [find](https://scholar.google.com/scholar?q=Z%2E+Wan%2C+Y%2E+Li%2C+Y%2E+Song%2C+H%2E+Wang%2C+L%2E+Yang%2C+M%2E+Schmidt%2C+J%2E+Wang%2C+W%2E+Zhang%2C+S%2E+Hu%2C+and+Y%2E+Wen%2E+Rema%3A+Learning+to+meta%2Dthink+for+llms+with+multi%2Dagent+reinforcement+learning%2E+arXiv+preprint+arXiv%3A2503%2E095)
28. R. Wang, J. Zhang, Y. Jia, R. Pan, S. Diao, R. Pi, and T. Zhang. [Theoremllama: Transforming general-purpose llms into lean4 experts](https://md.research.elamur.ai/free/en/papers/wang-2024-theoremllama-transforming-general-purpose-llms/). arXiv preprint arXiv:2407.03203, 2024.
29. R. Wang, R. Pan, Y. Li, J. Zhang, Y. Jia, S. Diao, R. Pi, J. Hu, and T. Zhang. Ma-lot: Multi-agent lean-based long chain-of-thought reasoning enhances formal theorem proving. arXiv preprint arXiv:2503.[03205, 2025](https://md.research.elamur.ai/free/en/papers/wang-2025-ma-lot-model-collaboration-lean/).
30. Z. Wu, S. Huang, Z. Zhou, H. Ying, J. Wang, D. Lin, and K. 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/).
31. Z. Wu, J. Wang, D. Lin, and K. Chen. [Lean-github: Compiling github lean repositories for a versatile lean prover](https://md.research.elamur.ai/free/en/papers/wu-2024-lean-github-compiling-github-lean/). arXiv preprint arXiv:2407.17227, 2024.
32. H. Xin, D. Guo, Z. Shao, Z. Ren, Q. Zhu, B. Liu, C. Ruan, W. Li, and X. Liang. [Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-advancing-theorem-proving/). arXiv preprint arXiv:2405.14333, 2024.
33. H. Xin, Z. Ren, J. Song, Z. Shao, W. Zhao, H. Wang, B. Liu, L. Zhang, X. Lu, Q. Du, et al. Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.[08152, 2024](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-v1-5-harnessing/).
34. R. Xin, C. Xi, J. Yang, F. Chen, H. Wu, X. Xiao, Y. Sun, S. Zheng, and K. Shen. [Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving](https://md.research.elamur.ai/free/en/papers/xin-2025-bfs-prover-scalable-best-first/). arXiv preprint arXiv:2502.03438, 2025.
35. K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. J. Prenger, and A. 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 (NeurIPS), 2023.
36. H. Ying, Z. Wu, Y. Geng, J. Wang, D. Lin, and K. Chen. [Lean workbook: A large-scale lean problem set formalized from natural language math problems](https://md.research.elamur.ai/free/en/papers/ying-2024-lean-workbook-large-scale-lean/). arXiv preprint arXiv:2406.03847, 2024.
37. W. Zeng, Y. Huang, Q. Liu, W. Liu, K. He, Z. Ma, and J. He. [Simplerl-zoo: Investigating and taming zero reinforcement learning for open base models in the wild](https://md.research.elamur.ai/free/en/papers/zeng-2025-simplerl-zoo-investigating-taming-zero/). arXiv preprint arXiv:2503.18892, 2025.
38. X. Zhao, W. Wu, J. Guan, and L. Kong. Promptcot: Synthesizing olympiad-level problems for mathematical reasoning in large language models. arXiv preprint arXiv:2503.02324, 2025. [find](https://scholar.google.com/scholar?q=X%2E+Zhao%2C+W%2E+Wu%2C+J%2E+Guan%2C+and+L%2E+Kong%2E+Promptcot%3A+Synthesizing+olympiad%2Dlevel+problems+for+mathematical+reasoning+in+large+language+models%2E+arXiv+preprint+arXiv%3A2503%2E02324%2C+2025%2E)
39. K. Zheng, J. M. Han, and S. Polu. [Minif2f: a cross-system benchmark for formal olympiad-level mathematics](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/). arXiv preprint arXiv:2109.00110, 2021.

*Updated 3 November 2026*