Introduction

When building agent applications that depend on Lean 4 and Mathlib, letting the model output code directly without local validation often results in generated proofs that fail to compile. lean4-harness-plugin is a plugin for DeepSeek Harness (DSH). It connects the local Lean 4 validator with the agent in the Web Profile. After the model generates Lean 4 source code, the plugin calls the local Lean validator and returns the validation result to the model, including error messages, line numbers, column numbers, and cache status. The model then modifies the code and checks it again until Lean explicitly accepts it.

Core Features

The plugin provides the following core capabilities:

  • Full Lean 4 source code validation
  • Reuse of a resident Lean LSP process to avoid repeated startup
  • Structured return of errors, warnings, line numbers, and column numbers
  • Precise .olean cache checking for Mathlib modules
  • One-time user authorization and controlled minimal builds when Mathlib modules are missing
  • tactic state formatting
  • Tools: lean_check, lean_repl_request, lean_format_tactic_state

Prerequisites

Before installation, ensure that the environment meets the following requirements:

  • Operating System: Windows 11 only
  • Node.js: >= 22.19.0
  • DeepSeek Harness: 0.1.3-alpha.2
  • Lean: leanprover/lean4:v4.26.0
  • Mathlib 4: Must be installed at the local path D:\mathlib4 and contain .olean cache files for the matching version

Installation and Enablement

The plugin is loaded through the DSH Bundle mechanism and does not need to be copied into the Harness packages/ directory.

Use the link: syntax to link the local repository to the Web Profile:

pnpm dsh plugin --profile web add 'link:D:\\lean4-harness-plugin'

After running the command above, the declaration for lean4-harness-plugin should be visible in the Web Profile configuration.

Typical Usage

Start a new conversation, give the model a math problem, and explicitly require it to call lean_check before completion.

You can give the model the following test requirements:

Please use Lean 4 and Mathlib to prove that natural number addition satisfies: 1 + 2 = 2 + 1.

Requirements:
1. Write the complete Lean 4 source code by yourself;
2. Choose the minimal necessary Mathlib submodules by yourself; do not use import Mathlib;
3. After generating the first version of the code, you must call lean_check;
4. If lean_check returns errors, modify the code based on the error messages and continue validation;
5. You may state that the proof is complete only after lean_check returns verified or verified_with_warnings.

Performance Note: The first lean_check may take from tens of seconds to several minutes. This is mainly used to load existing local .olean files into memory. Subsequent validations within the same Web service will reuse the resident Lean LSP process; reusedProcess in the result is usually true, so the speed is significantly improved.

Notes

  • The plugin does not “guess” for the model whether a proof is correct; it relies entirely on the local Lean validator.
  • The plugin depends on local Mathlib (D:\mathlib4) and will not download it during installation.
  • You must use the link: syntax to link the local repository to the Web Profile, rather than directly referencing a remote repository.
  • Windows 11 only.