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

OProver是由M-A-P开源社区与南京大学等团队提出的全开源Lean 4定理证明模型，创新性地将检索增强、编译器反馈与多轮修复内化至训练策略，解决训练与部署的‘策略错位’问题；32B版本在五项评测中三项第一、两项第二，全面超越671B的DeepSeek-Prover-V2，并同步开源OProofs语料库及多规模模型权重。