More details on DeepSeek-Prover-V2!
It comes in two sizes: 7B & 671B, and yes — the 7B variant beats Kimina-Prover Preview 72B! DeepSeek-Prover-V2 is an open-source LLM for formal theorem proving in Lean 4, initialized using a recursive pipeline powered by DeepSeek-V3.
DeepSeek-Prover-V2: Open-Source Lean 4 Theorem Proving LLM
By
–
