前言¶
用 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。
