DeepSeek-Prover-V2 es un modelo de lenguaje de código abierto a gran escala diseñado para la demostración formal de teoremas en Lean 4. Se inicializa con datos recopilados mediante un flujo de trabajo recursivo de demostración de teoremas basado en DeepSeek-V3. Realiza un entrenamiento de arranque en frío aprovechando la capacidad de DeepSeek-V3 para descomponer problemas complejos en múltiples subobjetivos. Las demostraciones de los subobjetivos resueltos se combinan con inferencias paso a paso de DeepSeek-V3 para generar datos iniciales para el aprendizaje por refuerzo. Esto integra razonamiento matemático formal e informal. El modelo resultante, DeepSeek-Prover-V2-671B, alcanza un rendimiento de vanguardia en la demostración de teoremas de redes neuronales, con una tasa de aprobación del 88,9 % en el test MiniF2F y resolviendo 49 de 658 problemas de PutnamBench. Presentamos una nueva métrica, ProverBench (325 problemas formalizados), que incluye 15 problemas de la reciente competencia AIME (24-25). Los resultados de la evaluación muestran que resuelve 6 de los 15 problemas AIME, lo que demuestra que la brecha entre el razonamiento matemático formal e informal se reduce significativamente en comparación con el método de votación mayoritaria de DeepSeek-V3 (que resuelve 8 problemas).