Summary

Overview

• OProver is a unified framework for agentic formal theorem proving in Lean 4 that treats proving as a multi-round refinement loop, where failed proof attempts are iteratively revised using retrieved compiler-verified proofs and Lean compiler feedback.
• The framework is trained through continued pretraining followed by iterative post-training that alternates agentic proving, supervised fine-tuning (SFT), and reinforcement learning (RL), with newly verified proofs and repair trajectories recirculated into the training corpus.
• OProofs, a large-scale Lean 4 corpus, contains 1.77M Lean statements, 6.86M compiler-verified proofs, and 1.07M agentic proving trajectories with serialized retrieval context, failed attempts, compiler feedback, and repairs.
• OProver-32B achieves state-of-the-art Pass@32 results on MiniF2F (93.3%), ProverBench (58.2%), and PutnamBench (11.3%), with second-best performance on MathOlympiad (22.8%) and ProofNet (33.2%)—more top placements than any prior open-weight whole-proof prover.
• Key ablations show that multi-turn compiler feedback is the dominant contributor to performance gains, with retrieval augmentation providing complementary benefits.

---

Introduction and Theoretical Foundation

Background

Formal theorem proving in systems like Lean 4 provides a rigorous setting for machine reasoning, where every proof step is mechanically verified by a small, trusted kernel. However, the field faces a critical challenge: most existing provers rely primarily on single-pass or best-of-N whole-proof generation, and retrieval and compiler feedback—when used at all—are typically applied as test-time heuristics rather than as part of a learned proving policy.

The Train–Inference Mismatch

A central motivation for OProver is the train–inference mismatch in existing systems. As the authors state:

"A prover trained mainly on finalized proofs sees compiler feedback and retrieved evidence only at deployment, in distributions it was never optimized for. Closing this train–inference mismatch requires training the prover to perform retrieval-grounded, feedback-conditioned refinement as part of its policy, not as a separate inference-time procedure."

Data Gap

Public formal theorem proving corpora focus on the end products of proving—formal statements and final compiler-verified proofs—but omit:

• Failed attempts
• Retrieved context
• Compiler diagnostics that drive proof repair in practice

This missing supervision prevents learning agentic self-correction.

---

Methodology

1. Agentic Proving Formulation

OProver formulates theorem proving as a bounded multi-round refinement process. At round $t$, the policy conditions on a state:

$$X_t = (s, \mathcal{R}_t, p_{t-1}, f_{t-1})$$

where $s$ is the target theorem statement, $\mathcal{R}_t$ is the retrieved proof context, $p_{t-1}$ is the previous proof attempt, and $f_{t-1}$ is the corresponding compiler feedback. The policy produces a revised proof attempt:

$$p_t \sim \pi(\cdot | X_t)$$

Key design choices:

• Compact interaction state: The policy conditions only on the most recent proof attempt and its feedback, not the full history
• Retrieval: Top-$k$ compiler-verified proofs are retrieved by semantic similarity using a sentence-embedding model trained on Lean theorem-proof pairs
• Raw compiler feedback: Diagnostics are passed directly as text without categorical encoding, preserving fine-grained information

2. OProofs Corpus Construction

OProofs is built through a two-branch pipeline:

3. Training Pipeline

Continued Pretraining (CPT): A one-time continued pretraining on a 65B-token mixture:

Iterative Post-Training (Algorithm 1):

1. Run multi-round agentic proving rollouts
2. Collect verified proofs and extract round-level repair examples
3. Select hard cases for RL
4. Update retrieval memory with new proofs
5. Apply SFT on repair examples, then GSPO (Group Sequence Policy Optimization) on hard cases

The reward function for RL assigns:

$$r_t = \begin{cases} 0.8 + 0.2 \cdot \mathbb{1}[\text{format correct}] & \text{if } \mathcal{V}(p_t) = \text{verified}, \\ 0.0 & \text{otherwise}. \end{cases}$$

---

Empirical Validation / Results

Corpus Statistics

OProofs contains:

• 1.77M unique Lean statements
• 6.86M compiler-verified proofs
• 4.33M proofs with retrieval context
• 869K with non-trivial compiler feedback
• 1.07M agentic proving trajectories (164K with multi-round repair)
• 280K round-level repair examples
• 51.8B Lean corpus tokens

The corpus spans Algebra (59.5%), Analysis (13.8%), Number Theory (13.0%), Geometry (6.8%), and Other (6.9%), with difficulty levels from Elementary (27.1%) to Graduate (4.8%).

Main Results (Pass@32, %)

† marks scores not re-evaluated under OProver's protocol.

Ablation Study

Key findings:

• Removing compiler feedback causes the largest degradation (up to 7.0 points on MathOlympiad)
• Retrieval provides smaller but consistent additional gains
• Both model sizes improve monotonically across post-training iterations

Test-Time Scaling

• Performance improves consistently with larger budgets $B$ (from 8 to 256) on all benchmarks
• Diminishing returns are observed, with the optimal allocation between refinement depth $R$ and sampling width $k$ being benchmark-dependent
• On easier benchmarks, $R=16$ is optimal; on the hardest (PutnamBench), the optimum saturates at $R=8$

---

Theoretical and Practical Implications

Theoretical Contributions

1. Unified framework: OProver demonstrates that retrieval, compiler feedback, and iterative repair can be unified into a single learned policy rather than treated as separate inference-time modules.

2. Co-evolution paradigm: The framework introduces a novel co-evolution loop where the prover and corpus improve jointly, with each iteration's verified proofs and repair trajectories enriching the training data for subsequent iterations.

3. Process-level supervision: By preserving multi-round interaction histories, OProofs provides richer supervision than final-proof-only corpora, enabling learning of proof repair strategies.

Practical Implications

1. Efficiency at scale: OProver-32B (dense) outperforms LongCat-Flash-Prover (560B MoE, ~17× more parameters) on most benchmarks, suggesting that agentic training signals can substitute for model scale.

2. Broad applicability: Gains span benchmarks of varying difficulty, from competition problems (MiniF2F) to undergraduate textbook formalizations (ProofNet) to Putnam problems.

3. Resource efficiency: Even OProver-8B outperforms Goedel-Prover-V2-32B on all five benchmarks despite having four times fewer parameters.

---

Conclusion

Summary

OProver presents a unified framework for agentic formal theorem proving in Lean 4, treating proving as a multi-round refinement loop where a trained policy revises failed attempts using retrieved proofs and compiler feedback. The accompanying OProofs corpus provides the trajectory-level supervision needed to train such policies, including failed attempts, retrieved context, and repair histories.

Key Contributions

1. A unified framework integrating retrieval, feedback, and iterative repair into a single learned policy
2. A large-scale corpus (OProofs) with 1.77M statements and 6.86M verified proofs with trajectory-level supervision
3. A co-evolution pipeline where prover and corpus improve jointly
4. State-of-the-art results among open-weight whole-proof provers across five benchmarks

Future Directions

The authors' work suggests several promising directions:

• Extending the framework to larger model scales
• Expanding to other proof assistants beyond Lean 4
• Investigating whether the co-evolution loop can continue improving without saturation at larger scales
• Applying the agentic training paradigm to other formal reasoning domains

The consistent improvements from iterative post-training and the effectiveness of compiler feedback suggest that "learning to repair" is a powerful paradigm for formal reasoning that may extend to other verifiable domains.