De acordo com a PANews, a DeepSeek lançou um novo modelo de código aberto, DeepSeek-Prover-V2-671B, focando em tarefas de prova de teoremas matemáticos. O modelo é construído sobre uma arquitetura de mistura de especialistas (MoE) e utiliza a estrutura Lean 4 para treinamento de raciocínio formal. Com uma escala de parâmetros de 671 bilhões, ele combina aprendizado por reforço e dados sintéticos em grande escala para melhorar significativamente as capacidades de prova automatizada. O modelo agora está disponível no Hugging Face, suportando tanto a implantação local quanto o uso comercial.