DeepSeek-Prover-V2: making the Lean kernel, not the model, the judge of correctness
DeepSeek's formal theorem proving model: a 671B MoE base shared with DeepSeek-V3 and Lean 4 as target language, so formal alignment on a flagship base. The core move is recursive subgoal decomposition at cold start: one-shot proofs of competition statements succeed so rarely that RL has almost no positive samples, so DeepSeek-V3 splits a statement into subgoals, a 7B model proves each, and the composed proofs become training data, trading decomposability for data density; the RL reward is binary and comes from the Lean kernel. Vendor-reported: MiniF2F-test 88.9% at pass@8192, PutnamBench 49/658 (about 7.4%), own ProverBench 325 problems. Read them together: MiniF2F is near saturation at that budget while hard Putnam problems drop an order of magnitude, and ProverBench is self-built and self-run. The public repo (about 1304 stars) ships a ZIP of proofs you can run through Lean, putting verifiability a tier above closed models. Limits: pass@8192 means eight thousand-plus candidates per problem, not comparable with pass@1. Not commensurable with Kimina-Prover's 92.2%, so we list both without ranking. Graded C (vendor-stated): nothing recomputed in our own Lean 4 + mathlib environment.