DeepSeek Prover-V2数学推理模型开源：参数规模突破，奥赛生实测“太棒”，中国AI再获国际关注

DeepSeek开源数学推理模型DeepSeek Prover-V2，提供7B和671B参数版本，专为Lean 4定理证明设计。该模型在MiniF2F测试中以82%通过率超越Kimina Prover，奥赛生实测表现优异，海外网友盛赞其自动化数学运算能力。技术上通过子目标分解和强化学习结合，统一非形式化与形式化推理，两种模式（CoT与非CoT）适应不同场景。在高中竞赛题、大学数学题等多场景表现卓越，7B模型甚至在某些测试中优于671B版本，显示高效推理能力。