TokenWave AI
TokenWave AI

▪  Research · Formal Theorem Proving

OProver

System paper · Formal Theorem Proving · updated 2026-08-04

Read the paperCode & Website

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

  1. 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.
  2. 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.
  3. 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.
  4. 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

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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

Figure 2 (paper, PDF p. 4): OProofs construction, retrieval- and compiler-guided agentic proving, and the iterative CPT/SFT/RL training loop that feeds verified proofs back into the corpus and retrieval memory. Source: paper.
Table 2 (paper, PDF p. 10): Pass@32 across MathOlympiadBench, MiniF2F, ProofNet, ProverBench, and PutnamBench for open reasoning models, whole-proof provers, and OProver-8B/32B; daggers mark baseline scores not rerun by the authors. Source: paper.

← Back to Research

Chart viewer