dsh-frontier-math

Readme

# dsh-frontier-math

一个面向 DeepSeek Harness 的前沿数学研究插件。它不会承诺“自动解决任意开放问题”，而是通过严格的选题、开放状态核实、声明依赖和独立验证门槛，提高产出真正新颖且可复核结果的概率。

## 核心原则

- **先查是否已经解决，再投入证明预算。**
- **只能判为“暂定仍开放”。** 自动检索无法证明整个文献中不存在结果。
- **反例和否证优先。** 不默认社区流行猜想为真。
- **实验不是证明。** 计算结果、自然语言推导和形式证书分别记录。
- **任何陈述改动都会使旧审计与证书失效。**
- **成果提交前必须做第二次新颖性复核。**

## 四个 DSH 工具

### `frontier_math_project`

创建、评分、查看和推进研究项目。问题必须通过以下硬门：

- 开放状态证据 ≥ 3/5；
- 陈述清晰度 ≥ 4/5；
- 独立验证路径 ≥ 3/5；
- 已有工作风险 ≤ 2/5；
- 综合机会分 ≥ 3.0。

### `frontier_math_prior_art`

核实问题是否已解决。一次完整审计必须覆盖：

1. 精确陈述或独特片段；
2. 等价表述、对偶、强弱版本；
3. 原论文、维护问题库或专家页面的当前状态；
4. 最近预印本、论文和后续结果；
5. 证明、否证和反例搜索。

至少需要两个独立域名、两个来源类别、两个证据家族，以及一个权威来源。发现可信的已解、已否证、部分结果或状态冲突时，项目自动阻断，直到逐项比较假设、结论、参数范围和量词顺序。

搜索摘要只能用于发现线索。任何中高可信度分类都必须保存实际来源中的短证据摘录，以及定理号、章节、页码或问题库条目位置；缺少这两项时审计会拒绝该分类。子域名会按保守的可注册主域归并，不能用同一站点的多个镜像伪造独立来源。

### `frontier_math_claim`

记录猜想、经验发现、推导、反例和定理，并维护无环依赖图。依赖未验证时，结论不能标为已验证。

### `frontier_math_certificate`

记录 Lean、精确计算、SAT/SMT、区间算法、文献与专家复核证书。首版只记录独立验证结果，不执行任意命令。

## 安装

在本目录运行：

```powershell
npm run verify
dsh plugin --profile web add link:.
```

重启 DSH Web 后检查：

```powershell
dsh --profile web --dump-config
```

浏览器研究状态面板：

```text
http://127.0.0.1:3080/frontier-math
```

## 推荐工作流

1. 让模型创建项目并给出逐项选题评分。
2. 完成五类已有工作检索；逐条分类来源。
3. 对任何“已解决/部分解决/等价命题”来源写等价性说明。
4. 审计只能得到 `provisionally_open` 后才进入研究阶段。
5. 建立多个互相区别的证明、反例和构造路线。
6. 将核心步骤拆成声明依赖图，保存失败路线。
7. 用 Lean、精确程序或专家审查生成独立证书。
8. 成果打包前启动 `recheck`，重新完成五类检索。
9. 自动门槛通过后进入 `ready_for_expert_review`；最终仍由领域专家确认。

## 数据位置

默认位于：

```text
%DSH_HOME%/frontier-math
```

每个项目是一个带 schema 版本的 JSON 文件。写入采用同目录临时文件加原子替换；Web API 只读，不提供任意文件路径。

## API

- `GET /api/frontier-math/health`
- `GET /api/frontier-math/projects`
- `GET /api/frontier-math/project?id=<project-id>`
- `GET /frontier-math`

## DeepSeek V4 Pro 建议

- 模型：`deepseek-v4-pro`
- 推理档位：`max`
- 使用 DSH 原生工具调用，保留交错思考状态
- 让热工作集保持精炼；长期材料写入声明和证据台账
- 在重要阶段运行多个真正不同的候选路线

## 已知限制

- 自动检索有覆盖盲区，不能替代 MathSciNet、zbMATH、专业数据库或领域专家。
- 来源分类由模型完成，必须保留原始链接和理由供人检查。
- “价值”和数学等价性含专家判断，评分只用于排序。
- 首版不直接执行 Lean 或其他验证器；它记录外部运行形成的证书。
- JSON 存储适合个人研究组合，不面向大型多用户并发部署。

## 开发检查

```powershell
npm run verify
npm pack --dry-run
```

设计依据和研究证据见 `report-source.md` 与 `docs/plans/`。