形式化定理证明，一直是 LLM 公认最严苛的推理试金石，每一步推导都必须通过 Lean 4 内核的机器验证。

近两年，开源社区在 MiniF2F、PutnamBench 等 benchmark 上的成绩持续上升，但增长路径越来越趋同：扩模型、扩数据、部署阶段叠加检索和多轮修正。

一个关键问题始终存在，检索信号、编译器反馈和失败修复，大多只在部署时作为外部流程接入，模型在训练阶段并没有系统学习如何利用这些信号，形成了训练与部署之间的 " 策略错位 "。

为应对这一挑战，M-A-P 开源社区与南京大学等团队提出OProver——

一个将检索增强、编译器反馈与多轮修复直接内化到训练策略中的 Lean 4 定理证明框架。

在五个 Lean 4 whole-proof prover 评测中，OProver-32B 取得三项第一、两项第二：

MiniF2F（93.3）、ProverBench（58.2）、PutnamBench（11.3）领先 LongCat-Flash-Prover w/ TIR，并在全部五项评测中超越 671B 的 DeepSeek-Prover-V2。

研究团队同步开源 1.76M 条形式化陈述、6.80M 编译器验证证明的 OProofs 语料库，以及 8B/32B 共 7 个模型权重。

代码、权重与训练脚本已全面开源。

策略错位：训练与部署之间的核心矛盾

近年来的 Lean 4 prover 系统（Goedel-Prover-V2、DeepSeek-Prover-V2、Kimina-Prover 等）在 MiniF2F 上已经把 Pass@32 推到较高水平，同时也有工作开始引入检索、编译器反馈或 self-correction。

问题在于，这些信号主要作为部署阶段的增强流程，接在已经训练好的 prover 外部，而非从训练阶段就被纳入学习目标。

这就形成了错位：

训练阶段，模型主要看到清晰的 theorem → verified proof 监督对

部署阶段，系统却把检索到的相关证明、上一轮失败尝试和 Lean 编译器反馈重新提供给模型，要求进行多轮修复

OProver 的核心思路，是让训练目标与部署时的证明过程对齐：让模型在训练阶段就学习如何执行 agentic refinement loop，把多轮修正、检索相关证明和编译器反馈作为训练策略的一部分，而非部署阶段的外部包装。

轻量、可端到端训练

部署阶段：有限轮次修复循环

OProver 把定理证明建模为一个有限轮次的修复循环。

策略基于目标形式化陈述、检索记忆库中的 top-k 个编译器验证证明、上一轮证明尝试和 Lean 4 编译器返回的诊断信息，生成下一次证明尝试。任意一轮通过，整条 trajectory 即视为成功。

训练阶段：两阶段训练

持续预训练（CPT）：在约 65B token 的混合语料上预训练，其中约 30% 来自 OProofs 的 Lean 4 数据，20% 为代码数据（OpenCoder），40% 为数学语料（Nemotron-Math-4-Plus），10% 为长 CoT 数据

迭代后训练：交替进行 agentic proving rollout、SFT（基于 round-level 修复样本）和 RL（基于 GSPO 算法与难题集）

关键设计在于：检索结果、失败尝试和编译器反馈不再只是部署阶段临时接入的外部流程，而是被纳入模型要学习的证明策略。

数据与模型的协同进化

OProofs 语料库与 prover 策略在迭代中相互促进。

每轮迭代中，当前 prover 在题库上生成的新验证证明被加入 OProofs 并索引进检索记忆库；

修复 trajectory 成为下一轮 SFT 训练样本；尚未解决的 " 难题组 " 为下一轮 RL 提供训练信号。

数据、训练与策略，形成持续演化的闭环。

OProofs：面向 agentic prover 的 Lean 4 语料

研究团队同步构建并开源了 OProofs，包含约 1.76M 条形式化陈述、6.80M 条编译器验证证明。

其中 4.29M 条证明保留了检索到的相关证明上下文，859K 条样本包含此前失败尝试的 Lean 编译器反馈。模型不只看到 " 最终正确证明是什么 "，也能学习 " 证明失败后，如何利用检索结果和编译器反馈继续修复 "。

OProofs 由两条构建分支组成。

1、公开资源再证明

以 NuminaMath-LEAN、Lean-Workbook、Leanabell-Prover-FormalStmt 等公开 Lean 资源为起点，清洗去重后通过 agentic proving 重新生成并验证证明，同时收集检索上下文、失败尝试和修复轨迹。

2、自然语言到形式化

从 Common Crawl 和 GitHub 挖掘数学陈述，用 CriticLean 自动形式化为 Lean 4，再通过 agentic proving 流程生成并验证证明。

从覆盖范围看，OProofs 横跨多个数学方向：代数 60.1%、分析 13.7%、数论 13.0%、几何 6.8%。难度分布以 elementary（27.4%）和 high-school（48.9%）层级为主，同时包含 18.9% 的本科水平和 4.8% 的研究生水平问题。

五项评测三项第一、两项第二

研究团队在 MiniF2F、MathOlympiad、ProofNet、ProverBench、PutnamBench 五个 Lean 4 benchmark 上评估，默认报告 Pass@32，基于 n=64 条独立 multi-round rollouts 的无偏估计。

在 open-weight whole-proof prover 范围内，OProver-32B 有三项关键结论：

1、32B 全面超越 671B

OProver-32B 在全部五项评测中超越 DeepSeek-Prover-V2（671B），在 MiniF2F（93.3）、ProverBench（58.2）、PutnamBench（11.3）上同时领先 LongCat-Flash-Prover w/ TIR（560B）。

2、8B 打平 32B

OProver-8B 在五个 benchmark 上全部超越 Goedel-Prover-V2-32B，参数量少 4 倍。

3、迭代后训练持续增益

MiniF2F-Test 上，OProver-8B 从 79.5 提升至 91.8（+12.3），OProver-32B 从 84.7 提升至 93.3（+8.6）。

消融实验：检索与编译器反馈协同贡献

移除多轮 compiler feedback 会导致最大幅度下降：OProver-32B 在 PutnamBench 从 11.3 降至 7.0，在 ProofNet 从 33.2 降至 25.8。

进一步移除检索后，性能继续下降至 5.9 和 24.7。

这说明提升并非来自简单的 best-of-N 采样，而是来自检索增强的证明生成与编译器反馈引导的多轮修复之间的协同。

其中，Lean 编译器反馈提供主要修复信号；检索上下文提供相关证明结构和可参考的证明片段。

测试时扩展：更多推理预算稳定转化

随着推理预算从 8 增加到 256，OProver-32B 在五个 benchmark 上均呈稳定提升：MiniF2F 从 87.5 至 92.8，MathOlympiad 从 15.5 至 22.0，ProofNet 从 25.6 至 32.8，ProverBench 从 51.3 至 56.9，PutnamBench 从 6.4 至 11.3。

最优预算分配与 benchmark 难度相关：多数 benchmark 更偏向增加 refinement 深度，而 PutnamBench 这类低成功率难题需在修复深度与并行探索之间取得平衡。

开源与发布

研究团队同步开源了 OProver 的模型、数据与训练代码，覆盖不同训练阶段 checkpoint、OProofs 语料和训练 pipeline。

• m-a-p/OProver-32B / OProver-8B — 最终模型

• m-a-p/OProver-32B-Base / Round1 — 32B 各阶段 checkpoint

• m-a-p/OProver-8B-Base / Round1 / Round2 — 8B 各阶段 checkpoint

• m-a-p/OProofs — 1.76M statements / 6.80M proofs / 1.06M trajectories

当然，OProver 目前仍主要围绕 Lean 4 whole-proof proving 展开。

后续值得观察的是，这种 agentic refinement 框架能否迁移到 Coq、Isabelle 以及工程级 formal methods 工具，以及更长的数据与模型协同进化周期中性能提升会持续多久。

论文：https://arxiv.org/abs/2605.17283

代码：https://github.com/multimodal-art-projection/OProver

模型与数据：https://huggingface.co/collections/m-a-p/oprover