lean4-harness-plugin: Local Lean 4 Verification Plugin for DeepSeek Harness

`lean4-harness-plugin` is a plugin for DeepSeek Harness designed to address the problem that agent-generated Lean 4 code fails validation. It enables automatic code validation and correction by connecting a local Lean 4 validator with Web Profile. The plugin supports reusing the Lean LSP process, Mathlib cache checking, and structured error responses. It must be installed in a Windows 11 environment and links the local repository to Web Profile using the `link:` syntax. When using it, you must explicitly instruct the model to call `lean_check` and iteratively correct the code until validation passes.

Read More