Elamur Research⌕
☰
home / papers / 2025 / StepFun-Prover Preview: Let's Think and Verify Step by Step

StepFun-Prover Preview: Let's Think and Verify Step by Step

Paper · 2025 · Shijie Shang, Ruosi Wan, Yue Peng et al.

Summary

LLM-based provers for Lean 4 usually need dozens of sampled attempts to find a valid proof, and extra samples bring shrinking gains. The authors argue this happens because such models rarely exploit verifier feedback the way experienced Lean users do. StepFun-Prover Preview addresses this by letting the model decide on its own when to send a code sketch to a Lean4-REPL sandbox, read the output and revise. It alternates natural-language thinking, Lean snippets and execution results until it commits to a final proof.

Training starts from DeepSeek-R1-Distill-Qwen (7B and 32B) and proceeds in stages:

  • SFT on STP data;
  • a cold-start set combining roughly 8,000 multi-turn trajectories from Claude Sonnet 4 with cleaned Kimina-Prover-72B proofs;
  • a fusion step in which the model repairs Kimina's failed answers;
  • GRPO without a KL term, using a binary verification reward;
  • one more SFT and RL cycle.

The 32B model reaches 70.0% pass@1 on miniF2F-test and outperforms far larger systems. This suggests that feedback-driven proving can reduce sampling cost and make provers more practical for non-experts.

Key points

  • Results on miniF2F-test (Numina-corrected version, Lean 4.20.0, 20K-token budget, pass@1 averaged over 32 samples):
    • StepFun-Prover-Preview-7B: 66.0%
    • StepFun-Prover-Preview-32B: 70.0%
    • DeepSeek-Prover-V2-671B: 61.9%
    • Kimina-Prover-72B: 63.9%
  • Problem sources and filtering:
    • Sources: Lean Workbook, STP, and Numina Math 1.5 problems autoformalized with Kimina-Autoformalizer-7B.
    • DeepSeek-V3 removed tautological, contradictory, irrelevant or trivial statements.
  • Test-time scaling: accuracy of the 32B model rises from 58.3% at 4,096 generated tokens to 70.0% at 20,480.
  • Infrastructure and behavior:
    • Optimizations to the remote REPL server made multi-turn RL more than 10× faster.
    • Learned behaviors include fixing Lean warnings and restructuring proofs after 60-second timeouts.
  • Released resources: code on GitHub (stepfun-ai/StepFun-Prover-Preview) and weights on HuggingFace (StepFun-Prover-Preview-32B).

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 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

Cite

Cite as Shijie Shang, Ruosi Wan, Yue Peng, Yutong Wu, Xiong-hui Chen, Jie Yan and Xiangyu Zhang. 2025. StepFun-Prover Preview: Let's Think and Verify Step by Step. arXiv:2507.20199.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2507.20199 · arXiv 2507.20199

@misc{shang2025stepfun,
  title = {{StepFun-Prover Preview: Let's Think and Verify Step by Step}},
  author = {Shijie Shang, Ruosi Wan, Yue Peng, Yutong Wu, Xiong-hui Chen, Jie Yan and Xiangyu Zhang},
  year = {2025},
  doi = {10.48550/arxiv.2507.20199},
  eprint = {2507.20199},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2507.20199}
}

References

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

  1. Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-Kishky, Aiden Low, Alec Helyar, Aleksander Madry, Alex Beutel, Alex Carney, et al. Openai o1 system card. arXiv preprint arXiv:2412.16720, 2024.
  2. Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. DeepSeek-R1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948, 2025.
  3. Qwen Team. QwQ: Reflect deeply on the boundaries of the unknown. https://qwenlm.github.io/blog/qwq-32b-preview , 2024. ↗
  4. 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, Lo… — Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
  5. Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcemen… — DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
  6. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-Prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025.
  7. Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, Bohan Wang, Siran Wang, Luoxin Chen, Jiahui Wang, Haowei Chen, Allan Jie, Xinbo Zhang, Haocheng Wang, Luong Trung, Rong Ye, Phan Nhat Hoang, Huishuai Zhang, Peng Sun, and Hang Li. Solving formal math problems by decomposition and iterative reflection. arXiv p…
  8. 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é, Thibaut Barroyer, Ebony Zhang, Bolton Bailey, Frederick Pu, Marina Vinyes, Zhengying Liu, and Jia Li. Kimina-Prover: Applying test-time… find
  9. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In International Conference on Automated Deduction, pages 625–635. Springer, 2021. — The Lean 4 Theorem Prover and Programming Language (System Description)
  10. Huaiyuan Ying, Zijian Wu, Yihan Geng, Zheng Yuan, Dahua Lin, and Kai Chen. Lean Workbook: A large-scale Lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847, 2024.
  11. Kefan Dong and Tengyu Ma. STP: Self-play llm theorem provers with iterative conjecturing and proving. arXiv preprint arXiv:2502.00212, 2025.
  12. Aixin Liu, Bei Feng, Bing Xue, Bingxuan Wang, Bochao Wu, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, et al. Deepseek-V3 technical report. arXiv preprint arXiv:2412.19437, 2024. find
  13. Anthropic. System card: Claude Opus 4 & Claude Sonnet 4. https://www-cdn.anthr opic.com/4263b940cabb546aa0e3283f35b686f4f3b2ff47.pdf , 2025. ↗
  14. Jingcheng Hu, Yinmin Zhang, Qi Han, Daxin Jiang, Xiangyu Zhang, and Heung-Yeung Shum. Open-Reasoner-Zero: An open source approach to scaling up reinforcement learning on the base model. arXiv preprint arXiv:2503.24290, 2025. A read-eval-print-loop for lean 4.
  15. Salvatore Sanfilippo. Redis. https://redis.io. ↗
  16. OpenAI. Introducing openai o3 and o4-mini. https://openai.com/index/introduci ng-o3-and-o4-mini/ , 2025. ↗
  17. Qwen Team. QwQ-32b: Embracing the power of reinforcement learning. https://qwen lm.github.io/blog/qwq-32b/ , 2025. find
  18. 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. In Advances in Neural Information Processing Systems, NeurIPS 2022, 2022.
  19. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022.
  20. Google DeepMind. AI achieves silver-medal standard solving international mathematical olympiad problems. https://deepmind.google/discover/blog/ai-solves-imo -problems-at-silver-medal-level/ , 2024. ↗
  21. Zijian Wu, Suozhi Huan, 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.
  22. Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.03438, 2025.
  23. 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-ca… — DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
  24. Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. arXiv preprint arXiv:2303.04910, 2023.
  25. Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022. https://github.com/leanprover- ↗
  26. Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Heng Liao, and Xiaodan Liang. LEGO-Prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656, 2023.
  27. Gheorghe Comanici, Eric Bieber, Mike Schaekermann, Ice Pasupat, Noveen Sachdeva, Inderjit Dhillon, Marcel Blistein, Ori Ram, Dan Zhang, Evan Rosen, et al. Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities. arXiv preprint a…
  28. Ahmed El-Kishky, Alexander Wei, Andre Saraiva, Borys Minaiev, Daniel Selsam, David Dohan, Francis Song, Hunter Lightman, Ignasi Clavera, Jakub Pachocki, et al. Competitive programming with large reasoning models. arXiv preprint arXiv:2502.06807, 2025.
  29. OpenAI. Introducing Codex. https://openai.com/index/introducing-codex/ , 2025. ↗
  30. Zhenghai Xue, Longtao Zheng, Qian Liu, Yingru Li, Zejun Ma, and Bo An. Simpletir: End-to-end reinforcement learning for multi-turn tool-integrated reasoning. https://si mpletir.notion.site/report , 2025. Notion Blog. find
  31. Joykirat Singh, Raghav Magazine, Yash Pandya, and Akshay Nambi. Agentic reasoning and tool integration for llms via reinforcement learning. arXiv preprint arXiv:2505.01441, 2025. — [arXiv:2505.01441](https://arxiv.org/abs/2505.01441) find
  32. Shaokun Zhang, Yi Dong, Jieyu Zhang, Jan Kautz, Bryan Catanzaro, Andrew Tao, Qingyun Wu, Zhiding Yu, and Guilin Liu. Nemotron-Research-Tool-N1: Tool-using language models with reinforced reasoning. arXiv preprint arXiv:2505.00024, 2025. — [arXiv:2505.00024](https://arxiv.org/abs/2505.00024) find
  33. Jiazhan Feng, Shijue Huang, Xingwei Qu, Ge Zhang, Yujia Qin, Baoquan Zhong, Chengquan Jiang, Jinxin Chi, and Wanjun Zhong. ReTool: Reinforcement learning for strategic tool use in llms. arXiv preprint arXiv:2504.11536, 2025.
  34. Xuefeng Li, Haoyang Zou, and Pengfei Liu. ToRL: Scaling tool-integrated rl. arXiv preprint arXiv:2503.23383, 2025.
  35. Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-Prover-V2: The strongest open-source theorem prover to date,… find
  36. Xingguang Ji, Yahui Liu, Qi Wang, Jingyuan Zhang, Yang Yue, Rui Shi, Chenxi Sun, Fuzheng Zhang, Guorui Zhou, and Kun Gai. Leanabell-Prover-V2: Verifier-integrated reasoning for formal theorem proving via reinforcement learning. arXiv preprint arXiv:2507.08649, 2025. — [arXiv:2507.08649](https://arxiv.org/abs/2507.08649) find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/shang-2025-stepfun-prover-preview-let-s/