lean4-harness-plugin：DeepSeek Harness 的 Lean 4 本地驗證插件

`lean4-harness-plugin` 是 DeepSeek Harness 的一個插件，旨在解決智能體生成 Lean 4 代碼無法通過驗證的問題。它通過將本地 Lean 4 驗證器與 Web Profile 連接，實現代碼自動校驗與修正。 該插件支持複用 Lean LSP 進程、Mathlib 緩存檢查及結構化錯誤返回，需在 Windows 11 環境下安裝，並通過 `link:` 語法將本地倉庫鏈接到 Web Profile。使用時，需明確要求模型調用 `lean_check` 並循環修正直至驗證通過。