DeepSeek unveils 671 billion parameter model for math proofs

Chinese artificial intelligence company DeepSeek has released a new open-weight language model named Prover V2, which contains 671 billion parameters and is focused on verifying mathematical theorems.

The model was uploaded to Hugging Face on April 30 under the open-source MIT license.

According to DeepSeek, Prover V2 is capable of compressing mathematical knowledge into a format that allows it “to generate and verify proofs,” with potential uses in both education and research.

This model follows the company’s earlier versions, Prover V1 and Prover V1.5, which were introduced in August 2024.

The first version used the Lean 4 programming language to convert math competition problems into formal logic.

The new model is significantly larger than its predecessors, weighing approximately 650 gigabytes.

To manage its size, DeepSeek quantized the model’s weights to 8-bit floating point precision, reducing its memory requirements while maintaining performance.

The scale and parameter count of Prover V2 suggest that it may be based on DeepSeek’s previous model R1, which gained attention last year for rivaling OpenAI’s o1 model.

However, the company has not yet published a research paper explaining what changes were made in Prover V2.

Open-weight models like this allow AI to be run locally, rather than through a centralised server.

While some view this as a step toward broader accessibility, others have raised concerns about the lack of guardrails against misuse.

The release of R1 prompted security concerns and was referred to by some as China’s “Sputnik moment.”

DeepSeek’s move has been compared to Meta’s earlier decision to release its LLaMA models with open access.

As with many large language models, Prover V2 requires high-performance hardware and large amounts of RAM or GPU memory to operate efficiently.

At the time of release, no benchmark data or performance metrics for Prover V2 were made available.