Theo PANews, DeepSeek đã phát hành một mô hình mã nguồn mở mới, DeepSeek-Prover-V2-671B, tập trung vào các nhiệm vụ chứng minh định lý toán học. Mô hình này được xây dựng trên kiến trúc hỗn hợp chuyên gia (MoE) và sử dụng khung Lean 4 để đào tạo lý luận chính thức. Với quy mô tham số là 671 tỷ, nó kết hợp học tăng cường và dữ liệu tổng hợp quy mô lớn để nâng cao đáng kể khả năng chứng minh tự động. Mô hình hiện đã có sẵn trên Hugging Face, hỗ trợ cả triển khai cục bộ và sử dụng thương mại.