DeepSeek-Prover-V2 用递归子目标分解 + RL 桥接 informal reasoning 与 Lean proof construction

DeepSeek-Prover-V2 使用 DeepSeek-V3 递归分解复杂 theorem 为 subgoals，并把已解决 subgoals 的形式证明与 step-by-step reasoning 合成 cold-start data，再进行强化学习。671B 模型在 MiniF2F-test 报告 88.9% pass ratio，并解决 PutnamBench 658 题中的 49 题；作者同时发布包含 325 题的 ProverBench。