inoricon1/dsh-frontier-math

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、区间算法、文献与专家复核证书。首版只记录独立验证结果，不执行任意命令。

安装

在本目录运行：

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

重启 DSH Web 后检查：

dsh --profile web --dump-config

浏览器研究状态面板：

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；最终仍由领域专家确认。

数据位置

默认位于：

%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=
- GET /frontier-math

DeepSeek V4 Pro 建议

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

已知限制

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

开发检查

npm run verify
npm pack --dry-run

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