如何免费使用 DeepSeek-Prover-V2？

近日，Deepseek 发布了一个新模型，这是一个在数学推理方面表现卓越的模型，即 DeepSeek Prover V2。

DeepSeek-Prover-V2 是一个专门使用 Lean 4 证明助手进行形式化定理证明的高级语言模型。

简单来说， DeepSeek-Prover-V2 旨在支持数学家和计算机科学家创建和验证形式化证明。

可以将其视为以绝对逻辑精确性解决复杂数学问题。它利用 Lean 4（一种专门用于数学推理的编程语言）来确保证明的每一步都经过严格验证。

主要特点

• 规模庞大：该模型拥有6710亿参数，并使用专家混合(Mixture-of-Experts, MoE)架构，以高效处理复杂的数学推理任务。

• 递归定理证明流程：训练数据是通过递归定理证明过程生成的，将复杂问题分解为子目标。

• 专精于Lean 4：专为Lean 4中的形式化定理证明而定制，对形式化方法领域的学者和开发者很有用。