前言¶
用 DeepSeek Harness（DSH）做数学相关任务时，常见做法是临时让 agent 读一段草稿或 Lean 文件，对话结束便丢失目标、假设和已核验结论之间的脉络。换会话或改研究方向后，很难说明「上次证明了什么、在新前提下哪些结论仍成立」。Leanary（包名 dsh-leanary）是维护者 wytyKen 发布的工作流类插件：用户用自然语言给出问题或草稿，agent 接手并保存研究进展，对明确的形式命题调用本地 Lean 做核验。Lean 通过只说明对应命题在形式系统中成立；自然语言是否忠实对应、整个研究目标是否完成，仍需要在对话中解释。
这是什么¶
Leanary 的定位是「面向 DeepSeek Harness 的本地数学研究雏形」。正式名称 Leanary，npm 包名 dsh-leanary，当前版本 0.1.0-dev.2，许可证 MIT。在 SkillHub 社区目录中归类为工作流；目录页与 GitHub 源码相互独立，社区站点与 DeepSeek / 幻方无官方从属关系。DSH 生态遵循「一切皆插件」；安装前宜自行查看源码与许可证，并记住插件随当前 DSH 进程权限运行。
核心功能¶
资料中已说明的能力如下。
- 接手草稿：读取已有文字草稿及 Lean 文件，保存目标、假设、候选结论和下一步。
- Lean 核验：对明确的形式命题做完整类型与传递公理层面的核验，并保留实际命令、源码及本地导入依赖的快照。
- 延续任务：在原任务上继续工作，识别源码或依赖变化；保留旧证明，并说明它与新目标的关系。
当前验收范围以工作区本地模块及工具链库为主；大型 Mathlib、任意 Lake 布局、远程运行和长期自动研究尚未验收。同一工作区应由一个 DSH 实例写入研究记录，不承诺多进程并发修改同一任务的事务性。
环境与版本¶
维护者在 README 中写明已验证环境为 Windows、Node.js 24、DSH 0.2.1-rc.3 和 Lean 4.22.0。package.json 要求 node >= 24.0.0、dsh 0.2.1-rc.3。模型认证由 DSH 提供，插件不另建模型客户端；安装与本地 Lean 检查不启动模型，对话使用所选模型服务并产生其 API 费用。
上手前可在终端确认 DSH 与 Lean 可用：
dsh --version
lean --version
示例使用 Lean 4.22.0 时，可按 Lean 官方方式安装 elan 后固定工具链：
elan toolchain install leanprover/lean4:v4.22.0
安装与启用¶
独立试用优先阅读仓库内 docs/QUICKSTART.md。试用 ZIP 含安装用 .tgz、START_HERE.md 和可复制到新工作区的 example，不依赖开发目录链接。下面步骤来自该上手说明：解压后进入含 START_HERE.md、.tgz 和 example 的目录，以新配置名 leanary-trial 为例（若该名已存在，请换新名并在后续命令中一致使用）。
创建带默认配置的配置名只对尚未使用的新名执行一次；--from-default-profile 会重置同名配置。
dsh --profile leanary-trial --from-default-profile web --help
dsh plugin --profile leanary-trial add ./dsh-leanary-0.1.0-dev.2.tgz
第二条命令通过 DSH 插件包管理器安装 .tgz，不编译本插件源码。若安装提示 pnpm was not found，需为 DSH 准备可用的 pnpm 并加入 PATH。停用插件可使用：
dsh plugin --profile leanary-trial remove dsh-leanary
工作目录中的研究文件仍由用户自行保存。
典型用法¶
先做安装与配置，再复制示例并启动 DSH。
- 将试用包中的
example目录复制到自选的新工作目录（例如项目内的.cache/workspaces/math-first-task）。核验产物也会写在该工作区，无需把资料放到系统文档目录外的特殊位置。 - 启动配置并保持终端开启：
dsh --profile leanary-trial --port 3082
- 在 DSH 中明确打开刚复制的工作目录并新建会话，不要仅凭默认工作区标签推断路径。
- 发送接手请求（与仓库
examples/order-bound/README.md一致）：
请阅读 problem.md 和 OrderBound.lean，接手并核验这段草稿，说明已有结果和接下来可以研究什么。
示例研究整数在 a ≤ b 时 a + b ≤ 2b 及等号何时成立，用于熟悉流程而非提高数学难度。研究记录与源码快照位于工作区 .dsh/math/。关闭后可用同一配置、同一工作区恢复原会话，或在新会话中要求读取已有研究记录。
想试一次目标变化，可继续发送：
如果不再假设 a ≤ b，原来的上界还成立吗？请给出依据，并说明已有的等号条件是否仍成立。
预期上应区分：上界在去掉前提后不再保证，等号条件仍可能对整数成立；旧证明应保留在历史说明中，新目标单独记录。
适用场景与注意¶
适合：需要在 DSH 里把数学草稿、Lean 源码与对话进展绑在同一工作区，并对局部形式命题做本地 Lean 核验的开发者或研究者。
注意：
- 插件以当前 DSH 进程权限运行；Lean 执行与文件修改受 DSH 权限机制约束，插件不会自动扩大权限。
- 仅支持以工作区根为模块根的本地 Lean 及本地导入；依赖未就绪时的报错不能解释为命题被数学反驳。
- 提示找不到
lean时，在启动 DSH 的终端检查 PATH，必要时重启 DSH。 - 端口占用时可改用空闲端口，例如
--port 3083，不影响任务记录。
GitHub 仓库当前星标为 0；功能与边界以 README 与 docs/QUICKSTART.md 为准。
结尾¶
Leanary 把「接手草稿、持久化研究状态、Scoped Lean 核验、改目标时保留旧证明」串成一条可在 DSH 内重复走的工作流。若要查看分类与简介，可打开社区目录页 wytyKen/dsh-leanary；源码、试用打包说明与 order-bound 示例见 GitHub：wytyKen/dsh-leanary。
