前言¶
在構建依賴 Lean 4 和 Mathlib 的智能體應用時，直接讓模型輸出代碼而不進行本地驗證，往往會導致生成的證明無法通過編譯。lean4-harness-plugin 是 DeepSeek Harness（DSH）的一個插件，它將本地的 Lean 4 驗證器與 Web Profile 中的智能體連接起來。模型生成 Lean 4 源碼後，插件會調用本地 Lean 驗證器，並將驗證結果（包括錯誤信息、行號、列號和緩存狀態）返回給模型。模型據此修改代碼並再次檢查，直至 Lean 明確通過。
核心功能¶
插件提供以下核心能力：
- 完整 Lean 4 源碼驗證
- 常駐 Lean LSP 進程複用，避免重複啓動
- 結構化錯誤、警告、行號和列號返回
- 精確 Mathlib 模塊的 .olean 緩存檢查
- 缺失 Mathlib 模塊時的用戶一次授權與受控最小構建
- tactic state 格式化
- 工具：
lean_check、lean_repl_request、lean_format_tactic_state
前置條件¶
安裝前需確認環境滿足以下要求：
- 操作系統：僅支持 Windows 11
- Node.js：>= 22.19.0
- DeepSeek Harness：0.1.3-alpha.2
- Lean：leanprover/lean4:v4.26.0
- Mathlib 4：需安裝在本地路徑
D:\mathlib4，且包含匹配版本的 .olean 緩存文件
安裝與啓用¶
插件通過 DSH Bundle 機制加載，不需要複製到 Harness 的 packages/ 目錄。
使用 link: 語法將本地倉庫鏈接到 Web Profile：
pnpm dsh plugin --profile web add 'link:D:\\lean4-harness-plugin'
執行上述命令後，在 Web Profile 的配置中應能看到 lean4-harness-plugin 的聲明。
典型用法¶
新建對話，給模型數學題，並明確要求它在完成前調用 lean_check。
可以將以下測試要求交給模型：
請使用 Lean 4 和 Mathlib 證明自然數加法滿足：1 + 2 = 2 + 1。
要求：
1. 自行寫出完整 Lean 4 源碼；
2. 自行選擇最小必要的 Mathlib 子模塊，不要使用 import Mathlib；
3. 生成第一版代碼後，必須調用 lean_check；
4. 若 lean_check 返回錯誤，請依據錯誤信息修改並繼續驗證；
5. 只有 lean_check 返回 verified 或 verified_with_warnings 後，才能說明證明完成。
性能說明：第一次 lean_check 可能需要幾十秒到數分鐘，這主要用於將本地已存在的 .olean 文件讀入內存。同一 Web 服務中的後續驗證會複用常駐 Lean LSP 進程，結果裏的 reusedProcess 通常爲 true，速度會明顯提升。
注意事項¶
- 插件不替模型“猜”證明是否正確，完全依賴本地 Lean 驗證器。
- 插件依賴本地 Mathlib (
D:\mathlib4)，不會在安裝時下載。 - 必須使用
link:語法將本地倉庫鏈接到 Web Profile，而不是直接引用遠程倉庫。 - 僅支持 Windows 11。
