Elamur Research⌕
☰
home / papers / 2025 / Leanabell-Prover: Posttraining Scaling in Formal Reasoning

Leanabell-Prover: Posttraining Scaling in Formal Reasoning

Paper · 2025 · Jingyuan Zhang, Qi Wang, Xingguang Ji et al.

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

🏢KuaishouBeijing · China20 works · 116 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

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

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

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 . ↗
  2. AoPS. Art of problem solving. https://artofproblemsolving.com/ . Accessed: [date]. ↗
  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. 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
  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
  6. DeepMind. Alphaproof and Alphageometry, July 2024. URL https://deepmind.googl e/discover/blog/ai-solves-imo-problems-at-silver-medal-level/ . ↗
  7. K. Dong and T. Ma. Stp: Self-play llm theorem provers with iterative conjecturing and proving. 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. 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. 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.
  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. 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
  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. arXiv preprint arXiv:2412.20735, 2024.
  14. H. Lin, Z. Sun, Y. Yang, and S. Welleck. Lean-star: Learning to interleave thinking and proving. 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. 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. arXiv preprint arXiv:2503.20783, 2025.
  17. mathlib4. The math library of lean 4, 2025. URL https://github.com/leanprover-c ommunity/mathlib4 . ↗
  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)
  19. L. C. Paulson. Isabelle: A generic theorem prover. Springer, 1994. find
  20. S. Polu and I. Sutskever. Generative language modeling for automated theorem proving. 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. 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. 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. 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
  25. Q. Team. Qwq-32b: Embracing the power of reinforcement learning, March 2025. URL 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. 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
  28. R. Wang, J. Zhang, Y. Jia, R. Pan, S. Diao, R. Pi, and T. Zhang. Theoremllama: Transforming general-purpose llms into lean4 experts. 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.
  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.
  31. Z. Wu, J. Wang, D. Lin, and K. Chen. Lean-github: Compiling github lean repositories for a versatile lean prover. 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. 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.
  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. 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. 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. 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. 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
  39. K. Zheng, J. M. Han, and S. Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/zhang-2025-leanabell-prover-posttraining-scaling-formal/