GLM-5.2 is live. #1 throughput on OpenRouter, pay-per-token on FriendliAI. Try it today ➜
m-a-p
Available on FriendliAI
Run this model inference on single tenant GPU with unmatched speed and reliability at scale.
Run this model inference with full control and performance in your environment.
Model Details
Model Provider
m-a-p
Model Tree
Base
this model
Input Modalities
Text
Output Modalities
Text
Supported Functionality
Dedicated Endpoints
Container
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 |
Use OProver-8B or OProver-32B for proving. The Base / Round-N checkpoints are released for reproducibility and ablation studies.
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.
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:
(s, R, p_{t-1}, f_{t-1}) → p_t,
with cross-entropy loss only on the new attempt.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.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.
python
from transformers import AutoModelForCausalLM, AutoTokenizer# Pick any of: OProver-8B, OProver-32B, *-Base, *-Round1, *-Round2name = "m-a-p/OProver-8B"tok = AutoTokenizer.from_pretrained(name)model = AutoModelForCausalLM.from_pretrained(name, torch_dtype="bfloat16", device_map="auto")
python
from datasets import load_datasetds = 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.
bibtex
@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}}
| 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 |