DeepSeek AI has released DeepSeek-Prover-V2, an open-source language model designed for theorem proving in the Lean 4 formal language. The model aims to automate the generation of mathematical proofs, a task that requires precise logical reasoning over formal specifications.
The system works by combining recursive proof search with training data produced by DeepSeek-V3, and it applies reinforcement learning to refine its proof strategies. According to the release, this approach achieves top results on MiniF2F, a widely used benchmark for evaluating neural theorem provers.
Alongside the model, DeepSeek introduced a new benchmark for neural theorem proving. The release continues the company's broader effort to apply large language models to formal mathematics and automated reasoning.