China’s DeepSeek Unveils New Open-Source AI Model for Math Proof Verification

DeepSeek, a Chinese artificial intelligence development company, has released its latest large language model (LLM), Prover V2, under an open-source MIT license. This new model aims to address math proof verification and is available on the Hugging Face platform. 671 billion parameters distinguish Prover V2, marking a significant leap from previous versions, Prover V1 and Prover V1.5. The model leverages Lean 4 programming language for training.