# Process-Verified Reinforcement Learning for Theorem Proving via Lean arXiv: https://arxiv.org/abs/2606.20068 ยท HTML: https://mlsanity.com/paper/2606.20068/ ## Key facts - Cited by 7 papers in the map (data through 14 Oct 2026). - Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. - Builds on 30 of its 48 references that are in the map. - First posted on arXiv 18 Jun 2026. ## Placed in - LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/) ## Builds on (most cited first, 30 of 30) - [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022) - [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017) - [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021) - [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024) - [Training a Helpful and Harmless Assistant with Reinforcement Learning from Human Feedback](https://mlsanity.com/paper/2204.05862/) (2022) - [Beyond the 80/20 Rule: High-Entropy Minority Tokens Drive Effective Reinforcement Learning for LLM Reasoning](https://mlsanity.com/paper/2506.01939/) (2025) - [Process Reinforcement through Implicit Rewards](https://mlsanity.com/paper/2502.01456/) (2025) - [Improve Mathematical Reasoning in Language Models by Automated Process Supervision](https://mlsanity.com/paper/2406.06592/) (2024) - [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021) - [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020) - [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022) - [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025) - [Rewarding Progress: Scaling Automated Process Verifiers for LLM Reasoning](https://mlsanity.com/paper/2410.08146/) (2024) - [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022) - [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024) - [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022) - [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024) - [Free Process Rewards without Process Labels](https://mlsanity.com/paper/2412.01981/) (2024) - [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025) - [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025) - [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024) - [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025) - [Dense Reward for Free in Reinforcement Learning from Human Feedback](https://mlsanity.com/paper/2402.00782/) (2024) - [What is Wrong with Perplexity for Long-context Language Modeling?](https://mlsanity.com/paper/2410.23771/) (2024) - [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://mlsanity.com/paper/2505.05758/) (2025) - [Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs](https://mlsanity.com/paper/2506.19923/) (2025) - [Leanabell-Prover: Posttraining Scaling in Formal Reasoning](https://mlsanity.com/paper/2504.06122/) (2025) - [Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning](https://mlsanity.com/paper/2507.08649/) (2025) - [Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capability](https://mlsanity.com/paper/2505.23703/) (2025) - [Premise Selection for a Lean Hammer](https://mlsanity.com/paper/2506.07477/) (2025) ## Built on by (most cited first, 7 of 7) - [BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints](https://mlsanity.com/paper/2607.28110/) (2026) - [MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research](https://mlsanity.com/paper/2607.14582/) (2026) - [TRACE: Training Reasoning Agents for Causal Exploration with Synthesized Rewards](https://mlsanity.com/paper/2609.10315/) (2026) - [Reinforcement Learning from Intermediate Renders for Image-to-Code Generation](https://mlsanity.com/paper/2609.34587/) (2026) - [LeanPolish: Verified Supervision for Lean Proof Compression](https://mlsanity.com/paper/2609.38384/) (2026) - [ROUTEAUDIT: Interaction-Aware Identification for Budgeted Multi-Verifier Routing](https://mlsanity.com/paper/2610.02808/) (2026) - [LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification](https://mlsanity.com/paper/2610.17697/) (2026) ## Abstract (arXiv) While reinforcement learning from verifiable rewards (RLVR) typically has relied on a single binary verification signal, symbolic proof assistants in formal reasoning offer rich, fine-grained structured feedback. This gap between structured processes and unstructured rewards highlights the importance of feedback that is both dense and sound. In this work, we demonstrate that the Lean proof assistant itself can serve as a symbolic process oracle, supplying both outcome-level and fine-grained tactic-level verified feedback during training. Proof attempts are parsed into tactic sequences, and Lean's elaboration marks both locally sound steps and the earliest failing step, yielding dense, verifier-grounded credit signals rooted in type theory. We incorporate these structured rewards into a GRPO-style reinforcement learning objective with first-error propagation and first-token credit methods that balances outcome- and process-level advantages. Experiments with STP-Lean and DeepSeek-Prover-V1.5 show that tactic-level supervision outperforms outcome-only baselines in most settings, delivering improvements on benchmarks such as MiniF2F and ProofNet. Beyond empirical gains, our study highlights a broader perspective: symbolic proof assistants are not only verifiers at evaluation time, but can also act as process-level reward oracles during training. This opens a path toward reinforcement learning frameworks that combine the scalability of language models with the reliability of symbolic verification for formal reasoning.