OProver: A Unified Framework for Agentic Formal Theorem Proving
Recent progress in formal theorem proving has benefited from large-scale proof generation and verifier-aware training, but agentic proving is rarely integrated into prover training, appearing only at inference time. We present OProver, a unified framework for agentic formal theorem proving in Lean 4, in which failed proof attempts are iteratively revised using retrieved compiler verified proofs and Lean compiler feedback. OProver is trained through continued pretraining followed by iterative post-training: each iteration runs agentic proving, indexes newly verified proofs into OProofs and the retrieval memory, uses repair trajectories as SFT data, and uses unresolved hard cases for RL. OP...
| Authors | David Ma, Kaijing Ma, Shawn Guo et al. |
|---|---|
| Primary category | cs.CL |
| Published | 17 May 2026 |
| Last updated at source | 17 May 2026 |
Connected in the knowledge graph
- m-a-p/OProver-8BModel · cited by
Models and datasets referencing this paper
- m-a-p/OProver-8BModel
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 17 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.