mlsanityData to 14 Oct 2026

OProver: A Unified Framework for Agentic Formal Theorem Proving

arXiv 2605.17283 ↗First posted 17 May 2026cs.CL cs.AIcited by 7

On the map: LLM agents and tool use → Educational agents and math problem solving

Abstract (arXiv)

Recent progress in formal theorem proving has benefited from large-scale proof generation and verifier-aware training, but agentic proving is rarely integrated into prover training, appearing only at inference time. We present OProver, a unified framework for agentic formal theorem proving in Lean 4, in which failed proof attempts are iteratively revised using retrieved compiler verified proofs and Lean compiler feedback. OProver is trained through continued pretraining followed by iterative post-training: each iteration runs agentic proving, indexes newly verified proofs into OProofs and the retrieval memory, uses repair trajectories as SFT data, and uses unresolved hard cases for RL. OProofs is built from public Lean resources, large-scale proof synthesis, and agentic proving traces, containing 1.77M Lean statements, 6.86M compiler-verified proofs, and serialized trajectories with retrieved context, failed attempts, feedback, and repairs. Across five benchmarks, OProver-32B attains the best Pass@32 on MiniF2F (93.3%), ProverBench (58.2%), and PutnamBench (11.3%), and ranks second on MathOlympiad (22.8%) and ProofNet (33.2%) more top placements than any prior open-weight whole-proof prover.

Key facts. Cited by 7 papers in the map (data through 14 Oct 2026). Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use. Builds on 33 of its 37 references that are in the map. First posted on arXiv 17 May 2026.

Builds on

33 of 37 references.

Closest ancestors · 3

Same direction, newest first

  1. 2026TheoremForge: Scaling up Formal Data Synthesis with Low-Budget Agentic Workflow24 Jan
  2. 2025StepFun-Prover Preview: Let's Think and Verify Step by Step27 Jul
  3. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs24 Jun

Other references · 30

  1. 2025Group Sequence Policy Optimizationcited by 835
  2. 2025DeepSeek-V3.2: Pushing the Frontier of Open Large Language Modelscited by 815
  3. 2026Kimi K2.5: Visual Agentic Intelligencecited by 501
  4. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  5. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  6. 2020Generative Language Modeling for Automated Theorem Provingcited by 388
  7. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  8. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 287
  9. 2022Autoformalization with Large Language Modelscited by 263
  10. 2022HyperTree Proof Search for Neural Theorem Provingcited by 197
  11. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 197
  12. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
18 more
  1. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 180
  2. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 165
  3. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 154
  4. 2024How to Train Long-Context Language Models (Effectively)cited by 146
  5. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
  6. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  7. 2024OpenCoder: The Open Cookbook for Top-Tier Code Large Language Modelscited by 130
  8. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 119
  9. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 101
  10. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 84
  11. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 79
  12. 2025Nemotron-CC-Math: A 133 Billion-Token-Scale High Quality Math Pretraining Datasetcited by 38
  13. 2024InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Searchcited by 34
  14. 2025Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learningcited by 27
  15. 2025CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalizationcited by 16
  16. 2025Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Provingcited by 12
  17. 2025Autoformalizer with Tool Feedbackcited by 7
  18. 2026LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learningcited by 7

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2026: 7.

7 papers.

  1. 2026BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprintscited by 2
  2. 2026VALG: An Agentic System for ML Theory Researchcited by 2
  3. 2026AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Languagecited by 1
  4. 2026Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verificationcited by 1
  5. 2026AutoGraphForge: Towards Automated Graph Theory Discoverycited by 0
  6. 2026Cost-Efficient Theorem Proving via Agent Orchestration in Program Verificationcited by 0
  7. 2026Humanize Olympiad Agents: A Multi-Session Workflow for Olympiad Problem Solving with Solve, Review, Wiki, Verifycited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2026Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
  2. 2026Agentic Proving for Program Verification
  3. 2026OpenProver: Agentic and Interactive Theorem Proving with Lean 4
  4. 2026Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
  5. 2026A Minimal Agent for Automated Theorem Proving
  6. 2026SorryDB: Can AI Provers Complete Real-World Lean Theorems?
  7. 2026Do Theorem Provers Need Theorem-Proving Agents? mini-Lean-agent: A Coding-Agent Baseline for Lean
  8. 2026Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement