mlsanityData to 7 Oct 2026

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

arXiv 2507.20199 ↗First posted 27 Jul 2025cs.AIcited by 12

On the map: LLM reasoning → Mathematical reasoning

also in 1 more
Abstract (arXiv)

We present StepFun-Prover Preview, a large language model designed for formal theorem proving through tool-integrated reasoning. Using a reinforcement learning pipeline that incorporates tool-based interactions, StepFun-Prover can achieve strong performance in generating Lean 4 proofs with minimal sampling. Our approach enables the model to emulate human-like problem-solving strategies by iteratively refining proofs based on real-time environment feedback. On the miniF2F-test benchmark, StepFun-Prover achieves a pass@1 success rate of 70.0%. Beyond advancing benchmark performance, we introduce an end-to-end training framework for developing tool-integrated reasoning models, offering a promising direction for automated theorem proving and Math AI assistant.

Key facts. Cited by 12 papers in the map (data through 7 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 24 of its 37 references that are in the map. First posted on arXiv 27 Jul 2025.

Builds on

24 of 37 references.

Closest ancestors · 5

Same direction, newest first

  1. 2025Solving Formal Math Problems by Decomposition and Iterative Reflection21 Jul
  2. 2025Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning11 Jul
  3. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition30 Apr
  4. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning15 Apr
  5. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving31 Jan

Other references · 19

  1. 2025DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learningcited by 6,146
  2. 2025Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilitiescited by 3,655
  3. 2024OpenAI o1 System Cardcited by 1,220
  4. 2024DeepSeek-V3 Technical Reportcited by 724
  5. 2025Open-Reasoner-Zero: An Open Source Approach to Scaling Up Reinforcement Learning on the Base Modelcited by 450
  6. 2025ReTool: Reinforcement Learning for Strategic Tool Use in LLMscited by 377
  7. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  8. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  9. 2025ToRL: Scaling Tool-Integrated RLcited by 166
  10. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  11. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  12. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
7 more
  1. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  2. 2025Competitive Programming with Large Reasoning Modelscited by 115
  3. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  4. 2025Agentic Reasoning and Tool Integration for LLMs via Reinforcement Learningcited by 107
  5. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
  6. 2025Nemotron-Research-Tool-N1: Exploring Tool-Using Language Models with Reinforced Reasoningcited by 67
  7. 2024InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Searchcited by 34

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 6; 2026: 6.

12 papers.

  1. 2025A Survey of Reinforcement Learning for Large Reasoning Modelscited by 175
  2. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 36
  3. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 18
  4. 2025EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficultycited by 7
  5. 2026LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learningcited by 6
  6. 2026OProver: A Unified Framework for Agentic Formal Theorem Provingcited by 6
  7. 2025LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)cited by 4
  8. 2025EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Provingcited by 1
  9. 2026Internalizing Agency from Reflective Experiencecited by 1
  10. 2026A Theoretical Framework for Self-Play Theorem Proving Algorithmscited by 1
  11. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  12. 2026RefineRL: Advancing Competitive Programming with Self-Refinement Reinforcement Learningcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
  2. 2021Proof Artifact Co-training for Theorem Proving with Language Models
  3. 2024Lean-STaR: Learning to Interleave Thinking and Proving
  4. 2025ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
  5. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoning
  6. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
  7. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
  8. 2025Theorem Prover as a Judge for Synthetic Data Generation