M-A-P 开源数学定理证明模型 OProver：32B 超越 671B，五项评测三项第一

M-A-P 开源社区与南京大学等团队发布 Lean 4 定理证明框架 OProver，将检索增强、编译器反馈与多轮修复内化到训练策略中。OProver-32B 在五个 Lean 4 whole-proof prover 评测中取得三项第一、两项第二，并在全部五项评测中超越 671B 的 DeepSeek-Prover-V2。