DeepSeek-Prover-V2通过OpenRouter平台在线免费调用

hbghlyj

一、什么是DeepSeek-Prover-V2-671B？

DeepSeek-Prover-V2-671B是一个具有6710亿参数的Mixture-of-Experts大型语言模型，由DeepSeek团队基于DeepSeek V3架构开发，专为形式化数学定理证明任务优化。
该模型在每次推理中从256个专家中激活8个专家，并支持FP8和BF16两种数值精度，以在保证性能的同时减少计算开销。
其上下文窗口长度最高可达163,840 tokens，使其能够处理大型数学文档和复杂证明链条。

二、通过OpenRouter平台在线调用DeepSeek-Prover-V2-671B

2.1 注册并获取API Key

访问OpenRouter官网并点击“Sign Up”进行注册，可以使用邮箱、Google或GitHub账号完成注册，推荐使用GitHub账号以加快流程。
登录后，在Dashboard中点击“Create API Key”按钮，为Key命名（如“ProverV2-Test”），复制并妥善保存该Key，后续API调用均需使用。

2.2 设置开发环境

在本地或云端搭建Python环境，并安装OpenAI兼容库，使用命令pip install openai可以确保与OpenRouter的API兼容，简化后续调用流程。

2.3 调用API生成证明

使用以下Python示例脚本向模型发送定理证明请求，并打印Lean 4格式的形式证明：

1. import openai
3. client = openai.OpenAI(
4.     base_url="https://openrouter.ai/api/v1",
5.     api_key="YOUR_API_KEY_HERE"
6. )
7. response = client.chat.completions.create(
8.     model="deepseek/deepseek-prover-v2:free",
9.     messages=[
10.         {"role": "system", "content": "你是一个专门使用Lean 4进行形式化定理证明的数学助手。"},
11.         {"role": "user", "content": "证明任意两偶数之和仍为偶数。"}
12.     ]
13. )
14. print(response.choices[0].message.content)

Copy the Code

可根据需求调整temperature和max_tokens等参数。

hbghlyj

为了评估 DeepSeek-Prover-V2 的基础证明能力，我们设计了如下简单示例：集合交集子集：证明任意两集合 A 和 B 的交集是 A 的子集；即 $A \cap B \subseteq A$。请提供完整的 Lean 4 证明及一句话解释关键步骤。

DeepSeek-Prover-V2 响应

1. theorem intersection_subset_left (A B : Type) (a : A) : A ∩ B ⊆ A := by
2.   intro x hx
3.   cases hx with
4.   | intro hx₁ hx₂ =>
5.     exact hx₁
6.   <;> simp_all
7. 关键步骤说明：使用 cases 策略对假设 hx : x ∈ A ∩ B 进行析构，将其拆分为 hx₁ : x ∈ A 和 hx₂ : x ∈ B 两部分，并直接使用 hx₁ 得出 x ∈ A。该策略详见[url=https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Cases.html?utm_source=chatgpt.com] Mathlib.Tactic.Cases 文档[/url]。
8. 一句话解释：由定义，$A \cap B$ 中的元素同时属于 A 和 B，因此必然属于 A。

Copy the Code

随后，我将该响应提交给 OpenAI o3 模型进行点评，其指出：

1. 应使用集合（Set α）而非类型（Type）来表示集合；
2. 可通过 .1 或 .left 直接提取 ⟨hx₁, hx₂⟩ 的第一分量，而不必使用 cases；
3. 去除多余参数和尾部 ;<;> simp_all，以获得更简洁的证明。

Copy the Code

在 Lean4 社区 Mathlib4 中，已内置如下引理，可直接复用：

1. theorem inter_subset_left {s t : Set α} : s ∩ t ⊆ s := fun _ => And.left

Copy the Code

因此，更简洁的 Lean 4 版本可写为：

1. theorem intersection_subset_left {α : Type*} (A B : Set α) : A ∩ B ⊆ A := by
2.   intro x hx
3.   exact hx.1          -- 或 exact hx.left

Copy the Code

此处 .1 即 And.left，用于直接提取合取中的左分量。

DeepSeek-Prover-V3 对上述 o3 反馈进行了修正，给出如下最终版本：

1. theorem intersection_subset_left {α : Type*} (A B : Set α) : A ∩ B ⊆ A := by
2.   intro x hx
3.   exact hx.1

Copy the Code

并同样附上一句话说明：“hx : x ∈ A ∩ B 可以视作二元组 ⟨hx₁, hx₂⟩，其中 hx₁ : x ∈ A 和 hx₂ : x ∈ B，因此 hx.1 直接得出 x ∈ A。”

OpenAI o3 对该最终版本发表评论称：

1. 正确性与简洁性：使用 hx.1（或 hx.left）是提取合取左分量的惯用写法；
2. 通用性：{α : Type*} 保持该引理对任意类型 α 的多态；
3. 风格建议：对于强调复用，可直接 exact Set.inter_subset_left，但展示一行推导更具教学意义。

Copy the Code

该示例展示了 DeepSeek-Prover-V2 被其它模型 OpenAI o3 纠正的过程。