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` 并循环修正直至验证通过。