Abstract
OProver is an agentic Lean 4 theorem-proving system whose retrieval, compiler feedback, and proof repair are represented during training as well as inference; it is not a new benchmark. A proving rollout conditions on a target theorem, semantically retrieved verified proofs, the most recent failed attempt, and raw Lean diagnostics, then revises the proof over a bounded number of rounds. Training starts with 65 billion tokens of Lean, code, mathematics, and long-chain reasoning, then alternates agentic rollouts, supervised learning on round-level repairs, and GSPO reinforcement learning on partially solved hard cases. The accompanying OProofs corpus contains 1.77 million unique statements, 6.86 million compiler-verified proofs, 1.07 million agentic trajectories, and 280,000 repair examples. OProver-8B and 32B are evaluated on five established Lean benchmarks under Pass@32 and compute-controlled protocols.
Contributions
- Uses the same retrieval-grounded, feedback-conditioned state at rollout collection, supervised fine-tuning, reinforcement learning, and inference, reducing the mismatch created when repair tools are added only at test time.
- Constructs OProofs from public Lean resources plus autoformalized Common Crawl and GitHub mathematics, retaining 1.77M statements, 6.86M verified proofs, 4.33M retrieval contexts, 869K examples with compiler feedback, and 164K multi-round repair trajectories.
- Introduces a co-evolution loop in which newly verified proofs expand both OProofs and its retrieval index, successful repair transitions become SFT examples, and theorem groups with non-trivial success rates supply group-relative RL signal.
- Evaluates dense 8B and 32B provers on MiniF2F, MathOlympiadBench, ProofNet, ProverBench, and PutnamBench. The 32B system reports Pass@32 of 93.3, 22.8, 33.2, 58.2, and 11.3 respectively under the paper's agentic protocol.
Method & evaluation
- OProofs has two construction branches. Public Lean statements are deduplicated and proved with open provers; informal mathematics mined from Common Crawl and GitHub is filtered, autoformalized with CriticLean, proved agentically, and retained only after Lean 4 verification.
- At each proving round, a theorem–proof sentence encoder retrieves the top-k semantically related compiler-verified proofs. The policy receives those references together with the theorem, only the previous attempt, and unmodified Lean error text rather than the full history.
- A successful attempt terminates the rollout and enters the retrieval memory; a failed attempt is revised until the round budget is exhausted. A sample in evaluation is one complete multi-round rollout and succeeds when any round produces a Lean-verified proof.
- Continued pretraining uses 65B tokens: approximately 30% Lean data from OProofs, 20% OpenCoder code, 40% Nemotron-Math-4-Plus mathematics, and 10% ProLong-64K long-chain reasoning.
- Iterative post-training decomposes rollouts into mappings from theorem, retrieved context, previous attempt, and feedback to the next proof. These round-level examples train SFT; GSPO then pools rewards across attempts and rounds, assigning reward only to Lean-verified outputs, with a small format bonus.
- Evaluation uses 244 MiniF2F test problems, 360 MathOlympiadBench problems, 186 ProofNet theorems, 325 ProverBench problems, and 672 PutnamBench problems. Unless stated otherwise, Pass@32 is estimated from 64 independent rollouts.
Evaluation metrics
Pass@32 — Higher is better. The standard unbiased estimate of the probability that at least one of 32 samples proves a theorem, computed from 64 independent samples per statement unless noted. For OProver, each sample is a multi-round rollout and every accepted proof must compile in Lean 4. Score range: [0, 100].
BestPass(B) — Higher is better. Best success rate attainable under total test-time budget B, maximizing over allocations where refinement depth R multiplied by sampling width k equals B. It separates gains from agentic depth from gains due only to more samples. Score range: [0, 100].
Lean verification — Higher is better. Binary proof validity returned by the Lean 4 compiler. It is the success criterion for evaluation, the gate for adding proofs to OProofs, and the RL reward prerequisite; formatting receives additional reward only after verification succeeds. Score range: [0, 1].
Figures & tables
