Chinese artificial intelligence development company DeepSeek has released a new open-weight large language model (LLM).
DeepSeek uploaded its newest model, Prover V2, to the hosting service Hugging Face on April 30. The latest model, released under the permissive open-source MIT license, aims to tackle math proof verification.
DeepSeek-Prover-V2 HuggingFace repository. Source: HuggingFace
Prover V2 has 671 billion parameters, making it significantly larger than its predecessors, Prover V1 and Prover V1.5, which were released in August 2024. The paper accompanying the first version explained that the model was trained to translate math competition problems into formal logic using the Lean 4 programming language — a tool widely used for proving theorems.
The developers say Prover V2 compresses mathematical knowledge into a format that allows it to generate and verify