---
title: "Kimina-Prover Preview — paper by Wang et al. (2025)"
description: "Starting from Qwen2.5-72B, the authors first build a large pool of Lean 4 problems with a trained… 33 references, cited by 90 papers here."
authors: ["Haiming Wang", "Mert Unsal", "Xiaohan Lin", "Mantas Baksys", "Junqi Liu", "Marco Dos Santos", "Flood Sung", "Marina Vinyes", "Zhenzhe Ying", "Zekai Zhu", "Jianqiao Lu", "Hugues de Saxcé", "Bolton Bailey", "Chendong Song", "Chenjun Xiao", "Dehao Zhang", "Ebony Zhang", "Frederick Pu", "Han Zhu", "Jiawei Liu", "Jonas Bayer", "Julien Michel", "Longhui Yu", "Léo Dreyfus-Schmidt", "Lewis Tunstall", "Luigi Pagani", "Moreira Machado", "Pauline Bourigault", "Ran Wang", "Stanislas Polu", "Thibaut Barroyer", "Wen-Ding Li", "Yazhe Niu", "Yann Fleureau", "Yangyang Hu", "Zhouliang Yu", "Zihan Wang", "Zhilin Yang", "Zhengying Liu", "Jia Li"]
year: 2025
venue: "arXiv:2504.11354"
source: "https://arxiv.org/abs/2504.11354"
doi: "10.48550/arxiv.2504.11354"
arxiv: "2504.11354"
licence: "CC BY-NC-ND 4.0 (arXiv)"
licence_url: "https://creativecommons.org/licenses/by-nc-nd/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/wang-2025-kimina-prover-preview-large-formal/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/wang-2025-kimina-prover-preview-large-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/) / Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning

# Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning

**Authors:** [Haiming Wang](https://md.research.elamur.ai/free/en/authors/haiming-wang/), Mert Unsal, Xiaohan Lin, [Mantas Baksys](https://md.research.elamur.ai/free/en/authors/mantas-baksys/), Junqi Liu, [Marco Dos Santos](https://md.research.elamur.ai/free/en/authors/marco-dos-santos/), Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, [Jianqiao Lu](https://md.research.elamur.ai/free/en/authors/jianqiao-lu/), Hugues de Saxcé, Bolton Bailey, Chendong Song, [Chenjun Xiao](https://md.research.elamur.ai/free/en/authors/chenjun-xiao/), Dehao Zhang, Ebony Zhang, Frederick Pu, [Han Zhu](https://md.research.elamur.ai/free/en/authors/han-zhu/), [Jiawei Liu](https://md.research.elamur.ai/free/en/authors/jiawei-liu/), Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidt, [Lewis Tunstall](https://md.research.elamur.ai/free/en/authors/lewis-tunstall/), Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, [Stanislas Polu](https://md.research.elamur.ai/free/en/authors/stanislas-polu/), Thibaut Barroyer, [Wen-Ding Li](https://md.research.elamur.ai/free/en/authors/wen-ding-li/), Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, [Zihan Wang](https://md.research.elamur.ai/free/en/authors/zihan-wang/), [Zhilin Yang](https://md.research.elamur.ai/free/en/authors/zhilin-yang/), [Zhengying Liu](https://md.research.elamur.ai/free/en/authors/zhengying-liu/) and [Jia Li](https://md.research.elamur.ai/free/en/authors/jia-li/) · **Year:** 2025 · **Venue:** arXiv:2504.11354 · **Licence:** [CC BY-NC-ND 4.0 (arXiv)](https://creativecommons.org/licenses/by-nc-nd/4.0/)

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

**Citations:** 2 citations (OpenAlex, 2026-10-14) · [90](https://md.research.elamur.ai/free/en/papers/wang-2025-kimina-prover-preview-large-formal/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Earlier neural theorem provers for Lean 4 usually combined a language model with explicit search, such as best-first or Monte Carlo tree search. That approach is expensive, and it has not clearly improved as models get larger. In this technical report, the Numina and Kimi teams present Kimina-Prover Preview, which explores proofs inside its own long chain of thought instead. Starting from Qwen2.5-72B, the authors first build a large pool of Lean 4 problems with a trained autoformalizer. Next comes a short supervised warm-up on about 20K Claude-generated examples that mix informal reasoning with Lean snippets, blended with informal math data from Kimi k1.5. Large-scale RL follows, and only proofs that the Lean compiler accepts earn a reward. Format filtering keeps training from collapsing. The model scores 80.7% on miniF2F-test at pass@8192, ahead of the previous best (BFS-Prover, 72.95%), and does well even with few samples. Accuracy also rises with model size, which earlier provers did not show. This suggests that reasoning-focused RL can replace costly search in formal mathematics. Distilled 1.5B and 7B models are released openly.

## Key points
- **RL setup:** follows the Kimi k1.5 recipe. Each step takes 1,000 problems with 8 rollouts each, and the Lean compiler gives a 0/1 reward. KL coefficient τ = 0.4, learning rate 2×10⁻⁶. Samples with negative gradients are dropped with probability 0.5. Reasoning-block code must cover at least 60% of the final proof.
- **miniF2F results:** at pass@32, 68.85%, compared with 37.70% for Gemini 2.5 Pro and 24.59% for o3-mini. At pass@8192, 80.74% overall, 40% on the IMO subset and 86.67% on the AIME subset.
- **Test-time scaling:** during training, average output length grew from about 2,500 to over 10,000 tokens, and pass@32 rose from 61.8% to nearly 69%. Progress was uneven along the way.
- **Released resources:** Kimina-Autoformalizer-7B and the distilled Kimina-Prover 1.5B/7B models (built on Qwen2.5-Math-Instruct). Fixed versions of 8 unsolvable miniF2F problems are on the Numina HuggingFace repository. The Numina Lean Server is based on LeanREPL and verifies about 10× faster, up to 100 iterations/s on 64 cores.
- **Contamination control:** 13-gram decontamination was applied, and AMC12/AIME/IMO items that overlap with miniF2F-test were removed from the Numina Math 1.5 training data.

*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 (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 18,614 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 17,965 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 321 works

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

## Cite

Cite as: Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidt, Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang, Zhengying Liu and Jia Li. 2025. Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning. arXiv:2504.11354.

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

```bibtex
@misc{wang2025kimina,
  title = {{Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning}},
  author = {Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco {Dos Santos}, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues {de Saxcé}, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidt, Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang, Zhengying Liu and Jia Li},
  year = {2025},
  doi = {10.48550/arxiv.2504.11354},
  eprint = {2504.11354},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2504.11354}
}
```

- [← previous ToolRL: Reward is All Tool Learning Needs](https://md.research.elamur.ai/free/en/papers/qian-2025-toolrl-reward-all-tool-learning/)
- [next → Qwen-Image Technical Report](https://md.research.elamur.ai/free/en/papers/wu-2025-qwen-image-technical-report/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/)

## References

33 references, 17 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. [https://anthropic.com/claude-3-7-sonnet-system-card](https://anthropic.com/claude-3-7-sonnet-system-card). 2025. [↗](https://anthropic.com/claude-3-7-sonnet-system-card)
2. Azerbayev, Zhangir et al. [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/). 2023. arXiv: 2302.12433 [cs.CL]. URL : https://arxiv.org/abs/2302.12433. [↗](https://arxiv.org/abs/2302.12433)
3. Deepmind. 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/](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/). [↗](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/)
4. DeepSeek-AI. [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/). 2025. arXiv: 2501.12948 [cs.CL]. URL : https://arxiv.org/abs/2501.12948. [↗](https://arxiv.org/abs/2501.12948)
5. First, Emily et al. [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://md.research.elamur.ai/free/en/papers/first-2023-baldur-whole-proof-generation-repair/). 2023. arXiv: 2303.04910 [cs.LG]. URL : https://arxiv.org/abs/2303.04910. [↗](https://arxiv.org/abs/2303.04910)
6. Huang, Yinya et al. MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data. 2024. arXiv: 2402.08957 [cs.AI]. URL : https://arxiv.org/abs/2402.08957. [↗](https://arxiv.org/abs/2402.08957)
7. Jiang, Albert Q. et al. [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/). 2023. arXiv: 2210.12283 [cs.AI]. URL : https://arxiv.org/abs/2210.12283. [↗](https://arxiv.org/abs/2210.12283)
8. Jiang, Albert Q., Wenda Li, and Mateja Jamnik. Multilingual Mathematical Autoformalization. 2023. arXiv: 2311. 03755 [cs.CL]. URL : https://arxiv.org/abs/2311.03755. [↗](https://arxiv.org/abs/2311.03755)
9. Kimi-Team et al. “[Kimi k1.5: Scaling reinforcement learning with llms](https://md.research.elamur.ai/free/en/papers/kimi-team-2025-kimi-k1-5-scaling-reinforcement/)”. In: arXiv preprint arXiv:2501.12599 (2025).
10. Lample, Guillaume et al. “[HyperTree Proof Search for Neural Theorem Proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/)”. In: Advances in Neural Information Processing Systems. Ed. by S. Koyejo et al. Vol. 35. Curran Associates, Inc., 2022, pp. 26337–26349. URL : [https://proceedings.neurips.cc/paper_files/paper/2022/file/a8901c5e85fb8e1823bb…](https://proceedings.neurips.cc/paper_files/paper/2022/file/a8901c5e85fb8e1823bb…) [↗](https://proceedings.neurips.cc/paper_files/paper/2022/file/a8901c5e85fb8e1823bb…)
11. Lean FRO. A read-eval-print-loop for Lean 4. [https://github.com/leanprover-community/repl](https://github.com/leanprover-community/repl). 2023. [↗](https://github.com/leanprover-community/repl)
12. Li, Jia et al. NuminaMath. [https://github.com/project-numina/aimo-](https://github.com/project-numina/aimo-) progress- prize/blob/main/ report/numina_dataset.pdf. GitHub repository. 2024. [↗](https://github.com/project-numina/aimo-)
13. Li, Yang et al. [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/). 2025. arXiv: 2412.20735 [cs.AI]. URL : https://arxiv.org/abs/2412.20735. [↗](https://arxiv.org/abs/2412.20735)
14. Lin, Haohan et al. “Lean-STaR: Learning to Interleave Thinking and Proving”. In: The Thirteenth International Conference on Learning Representations. 2025. URL : [https://openreview.net/forum?id=SOWZ59UyNc](https://openreview.net/forum?id=SOWZ59UyNc). [↗](https://openreview.net/forum?id=SOWZ59UyNc)
15. Lin, Yong 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/). 2025. arXiv: 2502. 07640 [cs.LG]. URL : https://arxiv.org/abs/2502.07640. [↗](https://arxiv.org/abs/2502.07640)
16. Moura, Leonardo de and Sebastian Ullrich. “The Lean 4 Theorem Prover and Programming Language”. In: Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, [Proceedings](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/).
17. Berlin, Heidelberg: Springer-Verlag, 2021, pp. 625–635. ISBN : 978-3-030-79875-8. DOI : 10.1007/978-3-030-79876-5_37. URL : https://doi.org/10.1007/978-3-030-79876-5_37. — [doi:10.1007/978-3-030-79876-5_37](https://doi.org/10.1007/978-3-030-79876-5_37) [↗](https://doi.org/10.1007/978-3-030-79876-5_37)
18. Nipkow, Tobias, Lawrence C Paulson, and Markus Wenzel. Isabelle/HOL: a proof assistant for higher-order logic. Vol. 2283. Springer Science & Business Media, 2002. [find](https://scholar.google.com/scholar?q=Nipkow%2C+Tobias%2C+Lawrence+C+Paulson%2C+and+Markus+Wenzel%2E+Isabelle%2FHOL%3A+a+proof+assistant+for+higher%2Dorder+logic%2E+Vol%2E+2283%2E+Springer+Science+%26+Business+Media%2C+2002%2E)
19. Numina. Numina Lean Server: Technical Report. arXiv preprint forthcoming. 2025. [find](https://scholar.google.com/scholar?q=Numina%2E+Numina+Lean+Server%3A+Technical+Report%2E+arXiv+preprint+forthcoming%2E+2025%2E)
20. OpenAI et al. [OpenAI o1 System Card](https://md.research.elamur.ai/free/en/papers/openai-2024-openai-o1-system-card/). 2024. arXiv: 2412.16720 [cs.AI]. URL : https://arxiv.org/abs/2412.16720. [↗](https://arxiv.org/abs/2412.16720)
21. Polu, Stanislas et al. [Formal Mathematics Statement Curriculum Learning](https://md.research.elamur.ai/free/en/papers/polu-2022-formal-mathematics-statement-curriculum-learning/). 2022. arXiv: 2202.01344 [cs.LG]. URL : https://arxiv.org/abs/2202.01344. [↗](https://arxiv.org/abs/2202.01344)
22. Qwen-Team. Qwen2.5: A Party of Foundation Models. Sept. 2024. URL : [https://qwenlm.github.io/blog/qwen2.5/](https://qwenlm.github.io/blog/qwen2.5/). [↗](https://qwenlm.github.io/blog/qwen2.5/)
23. Renshaw, David. Compfiles: Catalog Of Math Problems Formalized In Lean. [https://github.com/dwrensha/compfiles](https://github.com/dwrensha/compfiles). GitHub repository. 2024. [↗](https://github.com/dwrensha/compfiles)
24. Tsoukalas, George et al. [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://md.research.elamur.ai/free/en/papers/tsoukalas-2024-putnambench-evaluating-neural-theorem-provers/). 2024. arXiv: 2407.11214 [cs.AI]. URL : https://arxiv.org/abs/2407.11214. [↗](https://arxiv.org/abs/2407.11214)
25. Wang, Haiming et al. “Dt-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function”. In: Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 2023, pp. 12632–12646. [find](https://scholar.google.com/scholar?q=Wang%2C+Haiming+et+al%2E+%E2%80%9CDt%2Dsolver%3A+Automated+theorem+proving+with+dynamic%2Dtree+sampling+guided+by+proof%2Dlevel+value+function%E2%80%9D%2E+In%3A+Proceedings+of+the+61st+Annual+Meeting+of+the+Association+for+Computati)
26. Wang, Haiming, Huajian Xin, Zhengying Liu, et al. Proving Theorems Recursively. 2024. arXiv: 2405.14414 [cs.AI]. URL : https://arxiv.org/abs/2405.14414. [↗](https://arxiv.org/abs/2405.14414)
27. Wang, Haiming, Huajian Xin, Chuanyang Zheng, et al. [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://md.research.elamur.ai/free/en/papers/wang-2023-lego-prover-neural-theorem-proving/). 2023. arXiv: 2310.00656 [cs.AI]. URL : https://arxiv.org/abs/2310.00656. [↗](https://arxiv.org/abs/2310.00656)
28. Wang, Ruida et al. MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving. 2025. [arXiv: 2503.03205 cs.CL](https://md.research.elamur.ai/free/en/papers/wang-2025-ma-lot-model-collaboration-lean/). URL : https://arxiv.org/abs/2503.03205. [↗](https://arxiv.org/abs/2503.03205)
29. Wu, Zijian et al. InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems. 2024. [arXiv: 2410.15700 cs.AI](https://md.research.elamur.ai/free/en/papers/wu-2024-internlm2-5-stepprover-advancing-automated/). URL : https://arxiv.org/abs/2410.15700. [↗](https://arxiv.org/abs/2410.15700)
30. Xin, Huajian et al. [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/). 2024. arXiv: 2408.08152 [cs.CL]. URL : https://arxiv.org/abs/2408.08152. [↗](https://arxiv.org/abs/2408.08152)
31. Xin, Ran et al. BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving. 2025. arXiv: 2502.03438 [cs.AI]. URL : https://arxiv.org/abs/2502.03438. [↗](https://arxiv.org/abs/2502.03438)
32. Zhang, Jingyuan et al. Leanabell-Prover: Posttraining Scaling in Formal Reasoning. 2025. arXiv: 2504 . 06122 [cs.AI]. URL : https://arxiv.org/abs/2504.06122. [↗](https://arxiv.org/abs/2504.06122)
33. Zheng, Kunhao, Jesse Michael Han, and Stanislas 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/). 2022. arXiv: 2109.00110 [cs.AI]. URL : https://arxiv.org/abs/2109.00110. [↗](https://arxiv.org/abs/2109.00110)

*Updated 2 November 2026*