OProver: A Unified Framework for Agentic Formal Theorem Proving

Paper: OProver: A Unified Framework for Agentic Formal Theorem Proving — Multimodal Art Projection (M-A-P) — arXiv (link to be added on release)

Models & data: huggingface.co/collections/m-a-p/oprover — OProver-8B, OProver-32B, the OProofs corpus.

OProver is a unified framework for agentic formal theorem proving in Lean 4. Rather than treating retrieval, compiler feedback, and iterative repair as separate inference-time modules on top of a fixed prover, OProver unifies them with training and data construction into a single proving framework: failed proof attempts are iteratively revised using retrieved compiler-verified proofs and Lean 4 compiler feedback, and the same retrieval/feedback signals shape the prover's training policy.

Overview of OProver. OProofs Construction (top-left) builds a Lean-specific corpus from public Lean resources and autoformalized statements. OProver Agentic Proving (top-right) performs multi-round refinement under retrieval and Lean 4 compiler feedback. OProver Agentic Training (bottom) yields OProver-Base via a one-time CPT, followed by an iterative post-training loop in which agentic proving, SFT, and RL produce OProver_t+1 from OProver_t, while verified proofs are folded back into OProofs.

This repository is the official open-source release of the OProver pipeline. It contains every stage we use:

• Inference with iterative feedback refinement, RAG-augmented prompts, and online best-of-N.
• Verification through a Lean 4 server based on Kimina Lean Server.
• Continued pretraining (CPT), supervised fine-tuning (SFT), and reinforcement learning (RL) training stacks based on SteptronOSS and verl.
• Data tooling for dataset construction, prompt augmentation, retrieval-database management, and pass@k analysis.

The code in this repository is the cleaned snapshot we publish alongside the OProver paper; it preserves the exact pipeline used in the reported experiments.

Highlights

• Unified retrieval + feedback policy. OProver treats proving as a multi-round refinement loop and trains the prover end-to-end to use retrieved verified proofs and Lean compiler feedback as part of its policy — not as test-time heuristics.
• OProofs corpus. 1.77M Lean statements, 6.86M compiler-verified proofs, and serialized proving trajectories that record retrieved context, failed attempts, compiler feedback, and subsequent repairs. Released at m-a-p/oprover.
• Co-evolution pipeline. Iterative post-training where agentic proving, SFT, and RL alternate; newly verified proofs are indexed into the retrieval memory and repair trajectories feed the next training round.
• State-of-the-art Pass@32 among open-weight whole-proof provers. OProver-32B reaches 93.3 on MiniF2F, 58.2 on ProverBench, 11.3 on PutnamBench, 22.8 on MathOlympiad, and 33.2 on ProofNet. OProver-8B reaches 91.8 on MiniF2F, 9.0 on PutnamBench, 21.7 on MathOlympiad.

Main results

Pass@32 (%) on five Lean 4 theorem-proving benchmarks. Best in bold, second-best underlined. † marks scores not re-evaluated under our protocol.

Ablation

Removing multi-turn compiler feedback (-FB) or additionally removing retrieval augmentation (-FB, -RAG) hurts every benchmark at both model scales. Feedback is the dominant contributor.

Co-evolution across post-training iterations

Pass@32 on MiniF2F-Test improves monotonically as agentic proving, SFT, and RL iterate: OProver-8B rises 79.5 → 91.8 (Base → Round 3); OProver-32B rises 84.7 → 93.3 (Base → Round 2). Verified proofs and repair trajectories from each iteration are folded back into OProofs and the retrieval memory.

Test-time scaling

Both model sizes improve consistently as the total interaction budget $B$ grows; gains exhibit clear diminishing returns. Optimal allocation between refinement depth $R$ and sampling width $k = B/R$ depends on the per-chain success probability of the benchmark.

Repository layout

OProver/
├── components/
│   ├── inference/            # Online inference + iterative feedback (entry: run_tp_feedback.sh)
│   ├── kimina-lean-server/   # Lean 4 verifier service used by inference + RL
│   ├── verl/                 # RL + SFT training stack (vendored verl + OProver examples)
│   ├── steptronoss/          # CPT recipe + vendored SteptronOSS framework
│   └── data_tools/           # Offline dataset construction, pass@k, post-processing
├── docs/                     # Provenance and design notes
├── scripts/                  # Shared environment + utility scripts
├── data/                     # Default OPROVER_DATA_ROOT (populate locally)
├── outputs/                  # Default OPROVER_OUTPUT_ROOT (gitignored)
└── LICENSE

Each component has its own README.md with deeper details. The pointers below are the recommended entry points.

What you want to do	Where to look
Run inference with iterative feedback	components/inference/README.md
Start the Lean 4 verifier server	components/kimina-lean-server/README.md
Train via RL (GRPO/GSPO) or SFT	components/verl/README.md
Run continued pretraining	components/steptronoss/README.md
Build datasets / compute pass@k	components/data_tools/README.md

Quickstart

1. Clone

git clone https://github.com/multimodal-art-projection/OProver.git
cd OProver

2. Set up environment variables

All scripts honor a small set of OPROVER_* environment variables, with sensible defaults rooted at the repository top:

source scripts/oprover_env.sh

This exports OPROVER_ROOT, OPROVER_DATA_ROOT, OPROVER_OUTPUT_ROOT, and the per-component roots (OPROVER_INFERENCE_ROOT, OPROVER_VERL_ROOT, OPROVER_KIMINA_LEAN_SERVER_ROOT, OPROVER_STEPTRONOSS_ROOT, OPROVER_DATA_TOOLS_ROOT). Override any of them in your shell before sourcing.

3. Install component dependencies

Each component has its own Python environment requirements:

# Inference
pip install -r components/inference/requirements.txt

# RL / SFT training
pip install -r components/verl/requirements.txt
# (use components/verl/requirements-cuda.txt or requirements-npu.txt as needed)

# Lean verifier server
pip install -r components/kimina-lean-server/requirements.txt

Refer to the upstream repositories for non-Python dependencies (Lean 4 toolchain, Mathlib, etc.):

• Lean 4 + Mathlib: see components/kimina-lean-server/README.md.
• verl: see verl docs.
• SteptronOSS: see SteptronOSS.

4. Get the model

Download OProver-8B or OProver-32B from the HuggingFace collection and point your script to its path.

5. Run an end-to-end inference pass

After preparing a dataset under ${OPROVER_DATA_ROOT} and a model checkpoint:

# Start the Lean verifier (one-time, in a separate shell)
bash components/kimina-lean-server/server/proof/start_servers.sh

# Run iterative feedback inference (model, dataset, shard configurable inside the script)
bash components/inference/run_tp_feedback.sh

See components/inference/README.md for the full flow and configuration options.

Components

Inference (components/inference)

The online proof-search loop: prompt assembly, model rollout (vLLM / transformers backends), iterative feedback with verifier output, and best-of-N post-processing. Entry point: run_tp_feedback.sh.

Verifier (components/kimina-lean-server)

A FastAPI wrapper around the Lean 4 REPL, used by both online inference and RL rollouts. Supports the upstream /api/check endpoint and OProver's /verify endpoint.

Training (components/verl)

A reduced verl tree containing exactly the parts OProver uses:

• RL launchers under examples/grpo_trainer/prover_rl_new/ and the DAPO recipe.
• SFT launchers under examples/sft/oprover/.
• Data preprocessing helpers (examples/data_preprocess/lean4.py, merge scripts).
• OProver-specific reward managers, Lean4 reward score, feedback manager, RAG retrieval utilities.

Non-OProver verl recipes (prime, retool, spin, ...) have been removed; the verl/ package itself is otherwise upstream.

CPT (components/steptronoss)

Two things side-by-side:

• SteptronOSS/ — vendored copy of the SteptronOSS framework (no embedded .git, content unchanged).
• cpt/qwen3_oprover_cpt.py — the OProver continued-pretraining experiment that imports steptronoss.*.

Data tools (components/data_tools)

Offline scripts that don't belong to the inference launcher: pass@k aggregation, dataset construction helpers, prompt augmentation. Not required for either inference or training.

Models and data

Artifact	Description	Link
OProver-32B	Best Pass@32 on MiniF2F (93.3), ProverBench (58.2), PutnamBench (11.3).	HF Collection
OProver-8B	Smaller checkpoint; Pass@32 of 91.2 on MiniF2F.	HF Collection
OProofs	1.77M Lean statements, 6.86M compiler-verified proofs, serialized proving trajectories.	HF Collection

Provenance

See docs/PROVENANCE.md for the upstream sources of every vendored tree and the cleanup policy applied to this snapshot.

License

OProver-specific code is released under the Apache License 2.0. Vendored upstream trees retain their original licenses — see the individual component READMEs and components/*/LICENSE files.

Citation

If you use OProver in your research, please cite:

@article{oprover2026,
  title   = {OProver: A Unified Framework for Agentic Formal Theorem Proving},
  author  = {{Multimodal Art Projection}},
  year    = {2026},
  url     = {https://github.com/multimodal-art-projection/OProver}
}