PaperlayerView exact revision on arXiv

Source-linked AI summary

OProver: A Unified Framework for Agentic Formal Theorem Proving

David Ma, Kaijing Ma, Shawn Guo, Yunfeng Shi, Enduo Zhao, Jiajun Shi, Zhaoxiang Zhang, Gavin Cheung, Jiaheng Liu, Zili Wang

arXiv:2605.17283v1cs.CLcs.AI

TL;DR

Agentic theorem proving is rarely integrated into prover training, despite retrieval and compiler feedback being useful at inference time. OProver trains a Lean 4 prover to iteratively revise failed attempts using retrieved verified proofs and compiler feedback, achieving the strongest overall benchmark placement among open-weight whole-proof provers.

  • Problem

    Agentic retrieval, compiler feedback, and iterative repair are usually inference-time additions rather than capabilities learned within the prover’s policy.

  • Method

    OProver trains a Lean 4 policy through retrieval-grounded, feedback-conditioned refinement, supported by OProofs and iterative post-training from verified proofs and repair trajectories.

  • Results

    OProver-32B achieves the best Pass@32 on three of five benchmarks and the second-best on the other two, yielding more top placements than any other model.

  • Takeaways & Limitations

    Across benchmark families, the results suggest OProver’s proving strategy is broadly effective rather than specialized to a single family.

Abstract

from arXiv · show

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.

1. Introduction

OProver unifies retrieval, compiler feedback, and iterative proof repair with training and data construction for agentic Lean 4 theorem proving. Its companion corpus, OProofs, records proof-construction trajectories alongside large-scale formal statements and verified proofs.

  • Motivation: Lean 4 provides mechanically verified machine reasoning, but proofs must be fully formal and type-correct for acceptance.Verification is enforced by a small, trusted kernel.
  • Motivation: Existing systems typically add retrieval, compiler feedback, and iterative repair only at inference time rather than training the prover to use them.This leaves models trained mainly on finalized proofs exposed to retrieved evidence and compiler feedback only during deployment.
  • Motivation: Existing formal corpora mainly contain statements and final compiler-verified proofs, omitting failed attempts, retrieved context, and compiler diagnostics needed for proof repair.These omissions make them insufficient for training an agentic proving policy.
  • OProver: OProver unifies retrieval, compiler feedback, and iterative repair with training and data construction in a multi-round Lean 4 refinement loop.Each failed proof attempt is revised using retrieved compiler-verified proofs and Lean compiler feedback.
  • OProofs: 1.77M Lean statements and 6.86M compiler-verified proofs are contained in OProofs, alongside serialized trajectories of retrieved context, failures, feedback, and repairs.OProofs supports pretraining and the framework’s co-evolution loop, with data sourced from public Lean resources, proof synthesis, and OProver traces.

2. Methodology

OProver unifies theorem proving around a policy, retrieval memory, and Lean 4 verification, using compiler feedback and retrieved proofs for bounded multi-round repair. Its training co-evolves with OProofs through continued pretraining, agentic rollouts, SFT, and RL.

  • Framework components: OProver combines a proving policy, a retrieval memory of compiler-verified proofs, and the Lean 4 compiler as its verification environment.The policy is trained to use retrieval and compiler verification during proving.
  • Agentic proving: At each bounded round, the policy revises a proof using the target theorem, retrieved context, the previous attempt, and its compiler feedback.The interaction starts with empty proof and feedback states and ends upon verification or exhaustion of the round budget.
  • Agentic proving: The policy conditions only on the latest proof attempt and compiler feedback, preserving a compact state and a local correction signal across proving and training.The same state formulation is used for rollout collection, supervised fine-tuning, and reinforcement learning.
  • Agentic proving: At each round, semantic retrieval supplies top-k compiler-verified proofs from memory M, which expands with newly verified proofs during post-training.Compiler diagnostics are passed directly as raw textual feedback, retaining fine-grained information for targeted revisions.
  • OProofs construction: ∼1.5M Lean statements and ∼5.0M compiler-verified proofs make OProofs both training data and the source of retrieval memory, alongside serialized repair trajectories.The corpus records retrieved context, failed attempts, compiler feedback, and subsequent repairs.
  • Agentic training: Training first performs one-time continued pretraining, then iteratively alternates agentic proving with SFT and RL while expanding OProofs as the prover improves.SFT uses round-level repair examples extracted from rollouts, while RL further improves the policy after SFT.

3. Data Statistics

OProofs is a large-scale Lean 4 corpus combining public resources with model-generated compiler-verified proofs and agentic proving trajectories. Its data preserves retrieval, feedback, and repair supervision across a broad mathematical and difficulty spectrum.

  • Corpus Construction: OProofs combines public formal resources with proof synthesis and agentic proving pipelines, adding compiler-verified proofs and serialized trajectories decomposed into round-level repair examples.This design supports compiler-verified proof supervision and training from repair examples.
  • Corpus Size: 1.77M unique Lean statements are paired with 6.86M compiler-verified proofs and 1.07M agentic proving trajectories.These figures summarize the current Lean 4 component of OProofs.
  • Agentic Supervision: 4.33M proofs carry retrieved proof context, 869k carry non-trivial compiler feedback, and 280k round-level repair examples derive from 164k trajectories requiring repair.The frozen training snapshot contains 51.8B tokens, combining prompts and chain-of-thought tokenized with the Qwen3 tokenizer.
  • Coverage: Algebra accounts for 59.5% of the corpus, while High School problems constitute 48.9% across the reported domain and difficulty categories.The corpus also includes Analysis, Number Theory, Geometry, Other domains, and Elementary arithmetic, Undergraduate, and Graduate difficulty levels.

4. Experiments

OProver is evaluated across five Lean 4 theorem-proving benchmarks using agentic multi-round rollouts and Pass@32 as the primary metric. OProver-32B achieves the strongest overall results, benefits from increased test-time compute and iterative training, and relies primarily on compiler feedback with complementary retrieval gains.

  • Evaluation protocol: Unless otherwise noted, evaluation reports Pass@32 with n=64, counting a sample as successful when any attempt in its multi-round rollout is verified by Lean 4.The benchmark suite comprises MiniF2F, MathOlympiadBench, ProofNet, ProverBench, and PutnamBench, spanning competition, textbook, undergraduate, and difficult Putnam problems.
  • Benchmark results: OProver-32B records the best Pass@32 on MiniF2F (93.3%), ProverBench (58.2%), and PutnamBench (11.3%), and the second-best on MathOlympiad (22.8%) and ProofNet (33.2%).These results give OProver-32B three best and two second-best placements, more top placements than any other model in the comparison.
  • Benchmark results: Across five benchmarks, OProver-32B outperforms Goedel-Prover-V2-32B by 6.3 to 11.2 points per benchmark and surpasses the 671B DeepSeek-Prover-V2 on all five.Its closest competitor, LongCat-Flash-Prover, is a 560B Mixture-of-Experts model with roughly 27B active parameters per token.
  • Test-time scaling: Increasing OProver-32B’s budget from B=8 to B=256 raises scores from 87.5 to 92.8 on MiniF2F, 15.5 to 22.0 on MathOlympiad, 25.6 to 32.8 on ProofNet, 51.3 to 56.9 on ProverBench, and 6.4 to 11.3 on PutnamBench.Gains exhibit diminishing returns as the budget grows, while remaining robust across model sizes and benchmark types.
  • Iterative training: On MiniF2F-Test, iterative co-evolution improves OProver-8B from 79.5 at Base to 91.8 after Round 3 and OProver-32B from 84.7 to 93.3 after Round 2.Both model sizes improve monotonically across iterations.
  • Ablation study: Removing compiler feedback causes the largest degradation, while additionally removing retrieval produces smaller consistent drops, showing that feedback dominates and retrieval contributes complementary benefits.For OProver-8B, removing feedback lowers Pass@32 from 21.7 to 15.8 on MathOlympiad and from 9.0 to 5.7 on PutnamBench; for OProver-32B, removing retrieval causes drops from 0.5 to 1.7 points across listed benchmarks.

5. Related Work

Related work spans proof generation, guided and tactic-level search, whole-proof generation, verifier-driven repair, and data-centric supervision. OProver positions itself at their intersection by combining trajectory-level supervision with an iterative post-training loop tied to verified proofs and retrieval memory.

  • Proof generation and guided search: Neural theorem proving developed along proof-generation and guided-search directions, with early work modeling proofs as sequences and leveraging proof artifacts for supervision.GPT-f and PACT exemplify generated-sequence modeling and proof-artifact supervision, while HTPS represents search-based proving.
  • Tactic-level interaction and search: Lean theorem-proving research emphasizes tactic-level interaction, state-space search, retrieval-augmented environments, premise selection, critics, planners, and feedback-aware search.LeanDojo and ReProver highlighted premise selection, while subsequent systems extended interactive proving with learned guidance and search procedures.
  • Whole-proof generation: Whole-proof generation has advanced through synthetic theorem–proof data and proof-assistant feedback, followed by stronger models, longer-horizon reasoning, decomposition, and reinforcement learning.DeepSeek-Prover-V1.5 established the impact of synthetic data and assistant feedback, while Goedel-Prover, DeepSeek-Prover-V2, Kimina-Prover, and Seed-Prover extend the paradigm.
  • Repair and agentic proving: Verifier-driven work treats failed proofs as revisable, using repair models, informal reasoning, tool-integrated refinement, reinforcement learning, and agent-style coordination.Baldur introduced dedicated repair, while Lean-STaR, Leanabell-Prover-V2, StepFun-Prover, and Prover Agent develop increasingly agentic interaction patterns.
  • OProver’s position: OProver intersects these directions by preserving failed attempts, retrieved proof context, compiler feedback, and repairs as trajectory-level supervision while adding verified proofs to OProofs and retrieval memory.Its post-training loop couples data construction with policy improvement through newly verified proofs, repair examples, and harder unresolved cases.

6. Conclusion

OProver presents a unified Lean 4 framework that treats theorem proving as iterative repair, revising failed attempts with retrieved compiler-verified proofs and Lean compiler feedback. It is supported by OProofs, a large-scale corpus of Lean statements, verified proofs, and serialized agentic proving trajectories.

  • Framework: OProver is presented as a unified framework for agentic formal theorem proving in Lean 4.Its proving process is organized around repeated revision of failed attempts.
  • Framework: OProver unifies retrieval, Lean 4 compiler feedback, and iterative repair within a single proving policy.The policy operates as a multi-round refinement loop that revises failed proof attempts.
  • Training corpus: OProofs contains approximately 1.77M Lean 4 statements and 6.86M compiler-verified proofs.The corpus also includes serialized agentic proving trajectories recording retrieval contexts and failed attempts.

7. Contributions and Acknowledgments … A.2. Repair Instance Construction Details

The paper acknowledges M-A-P as a donation-run open-source AI research community and provides additional methodological details on retriever selection and repair-instance construction. Qwen3-8B-Embedding is selected as the default retriever, while filtered trajectory transitions supply deduplicated supervision for feedback-aware post-training.

  • 7. Contributions and Acknowledgments: M-A-P is a non-profit, donation-run open-source AI research community spanning foundation-model pretraining, large-scale data processing, coding, reasoning, and music generation.
  • A. Additional Method Details: The appendix covers retriever selection, repair-instance construction, data recirculation, training and evaluation hyperparameters, and pretraining-data recall.
  • A.1. Retriever Selection: The retriever comparison used a held-out set of 1,000 query statements and 9,000 candidate retrieval documents.
  • A.1. Retriever Selection: Qwen3-8B-Embedding spans approximately [0.20, 0.99] in similarity scores, versus Goedel-Prover-V2-8B’s concentrated [0.85, 0.99] range, providing more discriminative ranking.
  • A.1. Retriever Selection: 667 cases (66.7%) preferred Qwen3-8B-Embedding over Goedel-Prover-V2-8B across 1,000 GPT-4o pairwise comparisons, so OProver uses Qwen3-8B-Embedding by default.
  • A.2. Repair Instance Construction Details: For a T-round trajectory, each transition from (p_t−1, f_t−1) to p_t, paired with round-t retrieval context R_t, yields up to T−1 repair instances.
  • A.2. Repair Instance Construction Details: Instances are filtered for empty or malformed prior proofs, feedback exceeding 8,000 tokens, and revisions differing by fewer than 3 tokens; retained instances are deduplicated by exact (p−, f−, p+) match.These retained instances form the primary supervision substrate for feedback-aware post-training.

A.3. Data Recirculation Details

Each post-training iteration recirculates agentic proving rollouts into OProofs, retrieval memory, SFT repair data, and RL hard cases. Routing depends on rollout outcomes and the success rate of each theorem’s rollout group.

  • Routing and recirculation: Each post-training iteration routes rollouts into OProofs, retrieval memory, the SFT repair set, and the RL hard-case set.The recirculation pipeline indexes verified proofs, stores repair instances for supervised fine-tuning, and retains unresolved hard cases for reinforcement learning.
  • Routing and recirculation: Routing uses each rollout’s outcome and the success rate among n rollouts sampled for the same theorem.This group-level success rate determines whether theorem instances continue into subsequent training stages.
  • Routing and recirculation: Lean-verified proofs are appended to OProofs D_t+1 and re-indexed into retrieval memory M_t+1, while successful repairs enter SFT set B_t.Only rollouts yielding compiler-verified proofs contribute final proofs; repair instances are extracted from successful rollouts.
  • Routing and recirculation: Theorems with group success rates in (0, 1) are retained as hard cases H_t for the next RL round.These are theorems neither solved by all rollouts nor failed by all rollouts.
  • Routing and recirculation: The routing follows DAPO-style group filtering, excluding fully solved and fully failed groups to reduce gradient variance.The passage characterizes this reduction as empirical.

A.4. Training and Evaluation Hyperparameters

OProver uses distinct hyperparameter regimes for continued pretraining, supervised fine-tuning, reinforcement learning, and evaluation. Training and verification specify model-scale-dependent sequence, response, refinement, and server settings.

  • Continued pretraining: Continued pretraining uses a 65B-token mixture, AdamW, peak learning rate 5 × 10−5, cosine scheduling with 3% warmup, batch size 512, and sequence length 8192.These settings define OProver-Base pretraining.
  • Supervised fine-tuning: Supervised fine-tuning uses global sequence length 40,960 and batch size 64, with learning rates 2 × 10−5 for OProver-8B and 5 × 10−5 for OProver-32B.Cross-entropy loss is computed only on the target proof attempt p_t.
  • Reinforcement learning: Reinforcement learning uses GSPO with learning rate 2 × 10−6, batch sizes 256, 8 rollouts per theorem, a 14,000-token prompt limit, and model-specific response and refinement limits.Response lengths are 24,000 tokens for OProver-8B and 20,000 for OProver-32B; refinement rounds are 4 and 2, respectively.
  • Evaluation: Evaluation uses the same multi-turn proving interface as RL, with temperature 1.0, top-p 0.999, and a maximum response length of 32,000 tokens.The evaluation generation settings match the stated RL decoding temperature and top-p.
  • Evaluation: Proof verification uses the Kimina Lean server with Lean 4.15.0, proof reconstruction, fully explicit proofs, a 240s per-request timeout, and a heartbeat cap of 4M.These settings govern proof verification during evaluation.

A.5. Pretraining Data Recall … C.2. Case Study A: Putnam 1963 A3

The appendix describes how OProver recalls mathematics-adjacent pretraining data, formats prompts and raw Lean feedback, and uses retrieval-guided iterative repair. A Putnam 1963 A3 case study shows verifier feedback removing a local type error and restoring a compilable scaffold.

  • A.5. Pretraining Data Recall: OProver recalls mathematics-adjacent pretraining examples through a two-stage pipeline beginning with iterative fastText retrieval and seed-set expansion.Verified proofs and repair instances initialize the seed set; high-scoring candidates are merged back before retraining and another retrieval round.
  • A.5. Pretraining Data Recall: A small domain-trained embedding model filters recalled candidates by nearest-seed cosine similarity before the retained subset is mixed into CPT data.Candidates below threshold 𝜏 are discarded after the final fastText iteration.
  • B. Prompt Templates and Feedback Format: A single prompt template conditions each round on the Lean 4 target, top-k retrieved references, and the preceding proof attempt with Lean feedback.Round 1 leaves the previous-attempt and feedback fields empty, while later rounds request a concise proof plan and revision based on feedback.
  • B. Prompt Templates and Feedback Format: Lean feedback is serialized as the compiler’s raw plain-text diagnostic, preserving identifiers, expected and actual types, and goal contexts for targeted revision.The format avoids projecting diagnostics into a fixed taxonomy during inference.
  • C. Effectiveness of Agentic Reasoning: The agentic refinement loop iteratively revises candidate proofs using retrieved formal references and Lean verifier feedback rather than generating proofs in a single shot.The appendix presents qualitative examples of grounded repair behavior across rounds.
  • C.1. Roles of Retrieval and Compiler Feedback: Retrieved references ground lemma names and tactic idioms, suggest subgoal decompositions, and expose patterns that prevent formulation errors.Lean feedback complements retrieval by identifying verifier-side failures that map to local edits while preserving fine-grained diagnostic information.
  • C.2. Case Study A: Putnam 1963 A3: In the Putnam 1963 A3 case, feedback identified an ill-typed decide use and a failed assumption tactic, enabling removal of the local contradiction block.The repair restored type correctness and a viable compilable scaffold, though it did not complete the theorem.

C.3. Case Study B: Putnam 1986 A1

For Putnam 1986 A1, OProver repairs a directionally correct but under-specified algebraic proof by making bounds on y² explicit and splitting into sign-consistent cases, enabling arithmetic automation to establish the upper bound.

  • Initial attempt: The first-round proof fails because linarith cannot derive a contradiction from the implicit polynomial bounds.The feedback identifies an explicit decomposition of the polynomial constraint, rather than a different theorem, as the missing step.
  • Repair: The repair derives 4 ≤ y² ≤ 9 and then performs a bounded split over the two sign-consistent cases.The revised proof introduces interval constraints and separate upper and lower bounds for y before applying arithmetic automation.
  • Repair: The explicit decomposition produces subgoals aligned with arithmetic automation, allowing the upper-bound argument to go through.The revised structure replaces the implicit arithmetic state with usable interval and sign information.

C.4. Case Study C: Putnam 1992 A1 · C.5. Statement Labeling Prompt

Case C shows that interacting Lean failures require structural proof reorganization rather than isolated line edits, while the statement-labeling prompt classifies Lean 4 statements by mathematical domain and sophistication. The prompt produced 1.73M annotations, with 96.4% of responses parsing into valid JSON.

  • C.4. Case Study C: Putnam 1992 A1: Multiple interacting failures made Case C’s initial proof structurally invalid, including incomplete integer induction, inconsistent bindings, and incorrect equality applications.Lean reported invalid match expressions, metavariable-containing pattern types, function-equality type mismatches, missing congr_fun alternatives, and an unknown identifier.
  • C.4. Case Study C: Putnam 1992 A1: The repair reorganized the argument around explicit tuple destructuring, injectivity of f, parity analysis, and separate nonnegative and negative integer branches.The revised proof derives a recurrence and handles even and odd cases systematically; three induction sub-branches remain as sorry placeholders.
  • C.4. Case Study C: Putnam 1992 A1: Case C demonstrates that feedback-conditioned refinement matches repair granularity to the reported failure, scaling from local edits to multi-step structural revisions.Across the case studies, Lean feedback distinguishes ill-typed fragments, missing decompositions, and interacting structural failures.
  • C.5. Statement Labeling Prompt: The labeling prompt assigns each Lean 4 statement exactly one mathematical domain from 10 categories and one difficulty level from 4 tiers.Difficulty is based on mathematical sophistication required for the proof, not Lean proof length or syntactic complexity.
  • C.5. Statement Labeling Prompt: The four difficulty labels are Elementary, HighSchool, Undergraduate, and GraduatePlus, with guidance to choose the lower adjacent level when uncertain.Malformed, trivial, or otherwise nonmeaningful claims receive the Other domain and Elementary difficulty.
  • C.5. Statement Labeling Prompt: Examples map natural-number commutativity to Elementary Algebra, a binomial identity to HighSchool Combinatorics, compact-Hausdorff normality to Undergraduate Topology, and a zero-integral result to GraduatePlus Analysis.These examples illustrate classification by mathematical content and sophistication across four domains and levels.
  • C.5. Statement Labeling Prompt: 96.4% of labeling responses parsed as wellformed JSON with valid values, yielding 1.73M statement-level annotations.The prompt was run once per unique Lean 4 statement, and the annotations are summarized in Figure 3(b,c).
Loading 2605.17283v1…