OProver 把“失败—检索—编译器反馈—修复”直接写进训练循环，发布 686 万个 compiler-verified Lean proofs

OProver 提出统一的 agentic Lean 4 theorem-proving framework：失败 proof attempts 用检索到的 compiler-verified proofs 与 Lean compiler feedback 迭代修复；每轮 agentic proving 又反哺 OProofs retrieval memory、SFT repair trajectories 和 RL hard cases。OProofs 含约 177 万 Lean statements、686 万 compiler-verified proofs 及失败/反馈/修复轨迹；OProver-32B 在 MiniF2F、ProverBench、PutnamBench 等多个 whole-proof benchmarks 报告领先或次领先成绩。