Sponsored by
Vmake Labs Video Enhancer
m-a-p / OProver-8B-Base
Model's Last Updated: May 19 2026
text-generation
Introduction of OProver-8B-Base
Model Details of OProver-8B-Base
OProver
A unified framework for agentic formal theorem proving in Lean 4.
- 📄 Paper: OProver: A Unified Framework for Agentic Formal Theorem Proving ( arXiv )
- 📚 Collection: m-a-p/OProver
- 📦 Dataset: m-a-p/OProofs
OProver treats theorem proving as a multi-round refinement loop. Given a target theorem, the prover retrieves top-k compiler-verified proofs from a memory of prior proofs, generates a proof attempt, runs the Lean 4 compiler, and—on failure—revises the attempt using the compiler feedback in the next round. The same retrieval and feedback signals are baked into training, so the training-time interface matches the proving-time interaction.
Highlights
- State-of-the-art among open-weight whole-proof provers. OProver-32B attains 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). Even OProver-8B beats Goedel-Prover-V2-32B on all five benchmarks despite having 4× fewer parameters.
- Agentic proving is in the policy, not bolted on. Retrieval, multi-turn compiler feedback, and iterative repair are all part of the trained policy. Ablations show feedback is the dominant driver: removing it costs OProver-32B 4.9–7.4 Pass@32 points across benchmarks; removing retrieval on top adds 0.5–1.7 more.
- Co-evolving prover and corpus. Each post-training iteration runs agentic rollouts; verified proofs are added to OProofs and re-indexed for retrieval, repair trajectories become SFT data, and unresolved hard cases provide RL signal. MiniF2F-Test Pass@32 grows monotonically: OProver-8B 79.5 → 86.2 → 87.0 → 91.8 across rounds; OProver-32B 84.7 → 88.1 → 93.3.
What's in this release
The OProver collection ( m-a-p/OProver ) bundles the paper, the corpus, and seven model checkpoints covering both training stages and both model sizes:
| Repo | Stage | Size | Note |
|---|---|---|---|
| OProver-8B-Base | Continued pretraining only | 8B | Domain-adapted base; before SFT/RL |
| OProver-32B-Base | Continued pretraining only | 32B | Domain-adapted base; before SFT/RL |
| OProver-8B-Round1 | Post-training Round 1 | 8B | After first SFT+RL iteration |
| OProver-8B-Round2 | Post-training Round 2 | 8B | After second SFT+RL iteration |
| OProver-32B-Round1 | Post-training Round 1 | 32B | After first SFT+RL iteration |
| OProver-8B | Final | 8B | The 8B prover reported in the paper (Round 3) |
| OProver-32B | Final | 32B | The 32B prover reported in the paper (Round 2) |
| OProofs | Dataset | 6.86M proofs | Lean 4 corpus used for CPT, SFT, and the retrieval memory |
Use OProver-8B or OProver-32B for proving. The Base / Round-N checkpoints are released for reproducibility and ablation studies.
Dataset: OProofs
OProofs is a large-scale Lean 4 corpus that doubles as the retrieval memory at proving time. It is built from three sources: public Lean resources (NuminaMath-LEAN, Lean-Workbook, Leanabell-FormalStmt, Goedel-Pset, …), large-scale autoformalization + agentic proof synthesis from informal math mined on Common Crawl and GitHub, and traces from OProver's own agentic proving runs.
Training
Two stages, both anchored on OProofs.
1. Continued pretraining (one-time).
A 65B-token mixture of formal
Lean (≈30%, from OProofs), code (≈20%, OpenCoder), mathematics (≈40%,
Nemotron-Math-4-Plus), and long-CoT (≈10%, ProLong-64K). AdamW, peak LR
5e-5, cosine with 3% warmup, batch 512, sequence length 8192. Output:
OProver-{8B,32B}-Base
.
2. Iterative post-training. Each round runs:
- Agentic proving with the current prover on a theorem pool, producing multi-round rollouts conditioned on retrieved proofs and Lean feedback.
-
SFT
on round-level repair examples
(s, R, p_{t-1}, f_{t-1}) → p_t, with cross-entropy loss only on the new attempt. -
GSPO RL
on hard cases (groups with non-trivial pass-rate). Per-round
reward
r = 0.8 + 0.2·1[format ok]if Lean-verified, else 0; advantages are pooled across the n×R rounds for the same theorem. - Newly verified proofs and repair trajectories are folded back into OProofs and re-indexed into the retrieval memory for the next round.
Results
Pass@32 (n=64) across five Lean 4 benchmarks. Bold is best, underlined is second-best.
OProver-32B reaches three best and two second-best across five benchmarks — the most top placements of any model in the comparison, despite being a 32B dense model versus a 560B MoE or a 671B dense competitor.
Loading
from transformers import AutoModelForCausalLM, AutoTokenizer
# Pick any of: OProver-8B, OProver-32B, *-Base, *-Round1, *-Round2
name = "m-a-p/OProver-8B"
tok = AutoTokenizer.from_pretrained(name)
model = AutoModelForCausalLM.from_pretrained(name, torch_dtype="bfloat16", device_map="auto")
from datasets import load_dataset
ds = load_dataset("m-a-p/OProofs", split="train")
OProver is trained against a multi-round agentic interface: at each round the input includes the target Lean statement, top-k retrieved verified proofs, the prior proof attempt, and the Lean compiler feedback. See the paper §2.1 for the prompt template, and Appendix B for serialization details.
Citation
@article{ma2026oprover,
title = {OProver: A Unified Framework for Agentic Formal Theorem Proving},
author = {David Ma and Kaijing Ma and Shawn Guo and Yunfeng Shi and Enduo Zhao and Jiajun Shi and Zhaoxiang Zhang and Gavin Cheung and Jiaheng Liu and Zili Wang},
journal = {arXiv preprint arXiv:2605.17283},
year = {2026}
}
Runs of m-a-p OProver-8B-Base on huggingface.co
48
Total runs
0
24-hour runs
2
3-day runs
7
7-day runs
7
30-day runs
More Information About OProver-8B-Base huggingface.co Model
Url of OProver-8B-Base
OProver-8B-Base huggingface.co Url
Provider of OProver-8B-Base huggingface.co
Other API from m-a-p
Total runs:
20.6K
Run Growth:
20.1K
Growth Rate:
98.04%
Total runs:
4.7K
Run Growth:
-2.4K
Growth Rate:
-51.34%
Total runs:
3.6K
Run Growth:
2.8K
Growth Rate:
76.20%
Total runs:
2.1K
Run Growth:
588
Growth Rate:
30.69%
Total runs:
899
Run Growth:
314
Growth Rate:
34.93%
Total runs:
887
Run Growth:
176
Growth Rate:
19.84%
Total runs:
878
Run Growth:
693
Growth Rate:
78.93%
Total runs:
847
Run Growth:
312
Growth Rate:
36.84%
Total runs:
755
Run Growth:
-1.5K
Growth Rate:
-198.28%
Total runs:
629
Run Growth:
430
Growth Rate:
68.47%
Total runs:
611
Run Growth:
436
Growth Rate:
71.36%
Total runs:
513
Run Growth:
-442
Growth Rate:
-86.16%
Total runs:
511
Run Growth:
210
Growth Rate:
41.26%
Total runs:
478
Run Growth:
315
Growth Rate:
66.74%
Total runs:
404
Run Growth:
387
Growth Rate:
95.79%
Total runs:
399
Run Growth:
186
Growth Rate:
46.62%
Total runs:
349
Run Growth:
-91
Growth Rate:
-26.07%
Total runs:
247
Run Growth:
70
Growth Rate:
28.34%
Total runs:
191
Run Growth:
36
Growth Rate:
18.85%
Total runs:
161
Run Growth:
35
Growth Rate:
22.01%
Total runs:
155
Run Growth:
68
Growth Rate:
43.87%
Total runs:
115
Run Growth:
12
Growth Rate:
10.81%
Total runs:
112
Run Growth:
95
Growth Rate:
84.82%
Total runs:
100
Run Growth:
57
Growth Rate:
61.96%
Total runs:
97
Run Growth:
56
Growth Rate:
58.95%
Total runs:
89
Run Growth:
25
Growth Rate:
28.09%
Total runs:
69
Run Growth:
30
Growth Rate:
44.12%
Total runs:
63
Run Growth:
31
Growth Rate:
50.82%
Total runs:
53
Run Growth:
38
Growth Rate:
71.70%
Total runs:
51
Run Growth:
19
Growth Rate:
43.18%
Total runs:
48
Run Growth:
21
Growth Rate:
51.22%
Total runs:
46
Run Growth:
24
Growth Rate:
52.17%
Total runs:
45
Run Growth:
25
Growth Rate:
55.56%
Total runs:
45
Run Growth:
21
Growth Rate:
52.50%
Total runs:
45
Run Growth:
-19
Growth Rate:
-43.18%
Total runs:
45
Run Growth:
-14
Growth Rate:
-34.15%
Total runs:
44
Run Growth:
24
Growth Rate:
54.55%
Total runs:
44
Run Growth:
24
Growth Rate:
54.55%
Total runs:
43
Run Growth:
24
Growth Rate:
55.81%
Total runs:
43
Run Growth:
20
Growth Rate:
46.51%
Total runs:
42
Run Growth:
20
Growth Rate:
47.62%
Total runs:
41
Run Growth:
19
Growth Rate:
46.34%
Total runs:
41
Run Growth:
25
Growth Rate:
60.98%
Total runs:
41
Run Growth:
21
Growth Rate:
51.22%
Total runs:
40
Run Growth:
24
Growth Rate:
60.00%
Total runs:
40
Run Growth:
16
Growth Rate:
40.00%
Total runs:
40
Run Growth:
-11
Growth Rate:
-27.50%
Total runs:
39
Run Growth:
16
Growth Rate:
41.03%
Total runs:
37
Run Growth:
30
Growth Rate:
81.08%
Total runs:
36
Run Growth:
15
Growth Rate:
41.67%
Total runs:
35
Run Growth:
18
Growth Rate:
51.43%
Total runs:
35
Run Growth:
4
Growth Rate:
11.43%
Total runs:
34
Run Growth:
12
Growth Rate:
35.29%
Total runs:
33
Run Growth:
-1
Growth Rate:
-3.03%
Total runs:
33
Run Growth:
16
Growth Rate:
48.48%
Total runs:
33
Run Growth:
13
Growth Rate:
39.39%
Total runs:
32
Run Growth:
15
Growth Rate:
46.88%
Total runs:
31
Run Growth:
9
Growth Rate:
29.03%
Total runs:
31
Run Growth:
9
Growth Rate:
29.03%
Total runs:
31
Run Growth:
5
Growth Rate:
16.13%
Total runs:
30
Run Growth:
9
Growth Rate:
30.00%
Total runs:
29
Run Growth:
13
Growth Rate:
44.83%
Total runs:
27
Run Growth:
8
Growth Rate:
29.63%
Total runs:
27
Run Growth:
-16
Growth Rate:
-69.57%
Total runs:
26
Run Growth:
-5
Growth Rate:
-22.73%
Total runs:
25
Run Growth:
-6
Growth Rate:
-28.57%
Total runs:
25
Run Growth:
12
Growth Rate:
48.00%
Total runs:
24
Run Growth:
5
Growth Rate:
20.83%
Total runs:
24
Run Growth:
3
Growth Rate:
12.50%
Total runs:
23
Run Growth:
12
Growth Rate:
52.17%
Total runs:
23
Run Growth:
14
Growth Rate:
60.87%
Total runs:
23
Run Growth:
4
Growth Rate:
17.39%
Total runs:
23
Run Growth:
15
Growth Rate:
65.22%
Total runs:
22
Run Growth:
9
Growth Rate:
40.91%
Total runs:
22
Run Growth:
-9
Growth Rate:
-40.91%
Total runs:
22
Run Growth:
10
Growth Rate:
45.45%
Total runs:
21
Run Growth:
3
Growth Rate:
14.29%
Total runs:
20
Run Growth:
3
Growth Rate:
15.00%