671B-class MoE (37B nominal active backbone); 671.878B main non-scale tensors plus 13.477B exported MTP tensors; approximately 685.4B stored tensor elements including scales and routing buffers
128K-token evaluation limit; 163,840 configured positions
Apache-2.0 for the published checkpoint and code; early November 27 HF revisions carried MIT before the same-day Apache replacement, and upstream MIT notices remain relevant
Open-weight text-generation checkpoint for natural-language mathematical proofs, built on DeepSeek-V3.2-Exp-Base. The released final proof generator also performs proof verification; generator, verifier and meta-verifier are training roles, not a shipped two-model architecture. Its 61-layer MLA/MoE backbone selects eight of 256 routed experts plus one shared expert, and the released config includes DeepSeek Sparse Attention with a 64-head, 128-dimensional lightning indexer selecting 2,048 key-value entries. Weights use mixed FP8/BF16 with UE8M0 scales and include an auxiliary MTP block. Training alternates GRPO optimization of proof verification and generation: the initial verifier starts from a mathematics/code reasoning SFT checkpoint, learns expert proof scores of 0, 0.5 or 1, and uses meta-verification to penalize hallucinated defects. Each generator is initialized from the verifier; subsequent iterations consolidate verification and generation through rejection fine-tuning. Generator rewards combine proof quality (weight 0.76) with faithful self-assessment (0.24), encouraging a rigorous Solution followed by Self Evaluation and correction of identified errors. Scaled verification automatically labels difficult proofs, replacing human annotation in the last two training iterations. DeepSeek reports gold-level, not officially awarded medal, performance on IMO 2025 (five of six problems, 83.3% of points) and CMO 2024 (four fully solved plus partial credit, 73.8%), and 118/120 on Putnam 2024. These are high-compute search results: 64 initial proofs, 64 verification analyses per proof, refinement of the best 64 using eight analyses each, and up to 16 iterations; the same final generator supplies generation and verification, with mathematical experts grading selected proofs. Heavy-mode IMO-ProofBench expert evaluations report 99.0% Basic and 61.9% Advanced, not one-shot pass rates. The hardest IMO-level problems remain challenging, and natural-language self-verification is not formal proof certification. The report uses a 128K-token per-attempt limit; the larger positional config is not independently validated context support. November 27 is corroborated availability-by, with exact first public weight access unresolved. This card covers only the original final checkpoint, not separate unreleased training-stage verifiers, earlier 7B DeepSeekMath models or a hosted API alias.