Leanary：在 DSH 中持久化数学研究并用 Lean 核验形式命题

Leanary（dsh-leanary 0.1.0-dev.2）是 wytyKen 为 DeepSeek Harness 编写的工作流插件：接手文字草稿与 Lean 源码，在工作区 .dsh/math 保存目标与进展，并对明确形式命题做本地 Lean 4.22 核验。文章依据 README 与 QUICKSTART 说明环境（Node 24、DSH 0.2.1-rc.3）、试用 tgz 安装命令、order-bound 示例对话及当前不支持 Mathlib 等边界，并提醒插件随 DSH 权限运行。