DeepSeek Unveils Advanced Model for Mathematical Theorem Proving

According to PANews, DeepSeek has released a new open-source model, DeepSeek-Prover-V2-671B, focusing on mathematical theorem proving tasks. The model is built on a mixture of experts (MoE) architecture and utilizes the Lean 4 framework for formal reasoning training. With a parameter scale of 671 billion, it combines reinforcement learning and large-scale synthetic data to significantly enhance automated proving capabilities. The model is now available on Hugging Face, supporting both local deployment and commercial use.