Conform PANews, DeepSeek a lansat un nou model open-source, DeepSeek-Prover-V2-671B, axat pe sarcini de dovedire a teoremelor matematice. Modelul este construit pe o arhitectură de amestec de experți (MoE) și utilizează cadrul Lean 4 pentru antrenamentul raționamentului formal. Cu o scală a parametrilor de 671 de miliarde, combină învățarea prin întărire și date sintetice la scară mare pentru a îmbunătăți semnificativ capabilitățile de dovedire automată. Modelul este acum disponibil pe Hugging Face, susținând atât desfășurarea locală, cât și utilizarea comercială.