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 權限運行。