mlsanityData to 14 Oct 2026

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

arXiv 2504.11354 ↗First posted 15 Apr 2025cs.AIcited by 180

On the map: LLM reasoning → Mathematical reasoning

Abstract (arXiv)

We introduce Kimina-Prover Preview, a large language model that pioneers a novel reasoning-driven exploration paradigm for formal theorem proving, as showcased in this preview release. Trained with a large-scale reinforcement learning pipeline from Qwen2.5-72B, Kimina-Prover demonstrates strong performance in Lean 4 proof generation by employing a structured reasoning pattern we term textitformal reasoning pattern. This approach allows the model to emulate human problem-solving strategies in Lean, iteratively generating and refining proof steps. Kimina-Prover sets a new state-of-the-art on the miniF2F benchmark, reaching 80.7% with pass@8192. Beyond improved benchmark performance, our work yields several key insights: (1) Kimina-Prover exhibits high sample efficiency, delivering strong results even with minimal sampling (pass@1) and scaling effectively with computational budget, stemming from its unique reasoning pattern and RL training; (2) we demonstrate clear performance scaling with model size, a trend previously unobserved for neural theorem provers in formal mathematics; (3) the learned reasoning style, distinct from traditional search algorithms, shows potential to bridge the gap between formal verification and informal mathematical intuition. We open source distilled versions with 1.5B and 7B parameters of Kimina-Prover

Key facts. Cited by 180 papers in the map (data through 14 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 18 of its 31 references that are in the map. First posted on arXiv 15 Apr 2025.

Builds on

18 of 31 references.

Closest ancestors · 4

Same direction, newest first

  1. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoning8 Apr
  2. 2024HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving30 Dec
  3. 2024Lean-STaR: Learning to Interleave Thinking and Proving14 Jul
  4. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data14 Feb

Other references · 14

  1. 2025DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learningcited by 6,330
  2. 2025Kimi k1.5: Scaling Reinforcement Learning with LLMscited by 1,210
  3. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  4. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  5. 2022HyperTree Proof Search for Neural Theorem Provingcited by 197
  6. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 197
  7. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
  8. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 165
  9. 2022Formal Mathematics Statement Curriculum Learningcited by 142
  10. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
  11. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 109
  12. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 84
2 more
  1. 2023Multilingual Mathematical Autoformalizationcited by 39
  2. 2024Proving Theorems Recursivelycited by 26

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 80; 2026: 100.

180 papers.

Sort:

By area:

  1. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 287
  2. 2025The Landscape of Agentic Reinforcement Learning for LLMs: A Surveycited by 205
  3. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 154
  4. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 101
  5. 2025Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpeningcited by 80
  6. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 60
  7. 2025Aristotle: IMO-level Automated Theorem Provingcited by 58
  8. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Modelscited by 48
  9. 2026Code as Agent Harnesscited by 47
  10. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 44
  11. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  12. 2025Reinforcement Learning Meets Large Language Models: A Survey of Advancements and Applications Across the LLM Lifecyclecited by 35
38 more
  1. 2025CombiBench: Benchmarking LLM Capability for Combinatorial Mathematicscited by 31
  2. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 31
  3. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 31
  4. 2025The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofscited by 30
  5. 2025CLEVER: A Curated Benchmark for Formally Verified Code Generationcited by 29
  6. 2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Proverscited by 28
  7. 2025Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learningcited by 27
  8. 2025FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levelscited by 27
  9. 2025OJBench: A Competition Level Code Benchmark For Large Language Modelscited by 26
  10. 2026Advancing Mathematics Research with AI-Driven Formal Proof Searchcited by 23
  11. 2025Introducing LongCat-Flash-Thinking: A Technical Reportcited by 22
  12. 2025Adaptation of Agentic AI: A Survey of Post-Training, Memory, and Skillscited by 22
  13. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 21
  14. 2025Solving Inequality Proofs with Large Language Modelscited by 21
  15. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 21
  16. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 21
  17. 2025ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimizationcited by 20
  18. 2025Mathesis: Towards Formal Theorem Proving from Natural Languagescited by 18
  19. 2025ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddingscited by 18
  20. 2026A Minimal Agent for Automated Theorem Provingcited by 18
  21. 2026AI co-mathematician: Accelerating mathematicians with agentic AIcited by 17
  22. 2026MLS-Bench: A Holistic and Rigorous Assessment of AI Systems on Building Better AIcited by 17
  23. 2025CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalizationcited by 16
  24. 2025StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusioncited by 16
  25. 2025LLM/Agent-as-Data-Analyst: A Surveycited by 16
  26. 2025Physics Supernova: AI Agent Matches Elite Gold Medalists at IPhO 2025cited by 14
  27. 2025miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forwardcited by 14
  28. 2025ICPC-Eval: Probing the Frontiers of LLM Reasoning with Competitive Programming Contestscited by 13
  29. 2025StepFun-Prover Preview: Let's Think and Verify Step by Stepcited by 13
  30. 2025Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Provingcited by 12
  31. 2026AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithmscited by 12
  32. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworkscited by 12
  33. 2026LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalizationcited by 12
  34. 2025Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capabilitycited by 11
  35. 2025HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMscited by 11
  36. 2026Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verificationcited by 11
  37. 2025MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curationcited by 10
  38. 2026Scaling Self-Play with Self-Guidancecited by 10

50 most cited of 180 All 180 (JSON)

Similar, not cited

Close in wording, no citation either way

  1. 2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
  2. 2025Theorem Prover as a Judge for Synthetic Data Generation
  3. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
  4. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
  5. 2026Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning
  6. 2025Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection
  7. 2021Proof Artifact Co-training for Theorem Proving with Language Models
  8. 2025Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework