lean4-harness-plugin

When writing Lean 4 formal proofs with AI, the biggest risk is that the model has no real verification feedback: it can only guess whether a proof is correct from surface semantics, while formal mathematics demands certainty. lean4-harness-plugin closes this gap inside deepseek-harness: after the model generates or edits Lean source code, the plugin invokes a local Lean LSP process for full compilation, returning the actual pass status, error diagnostics, line and column numbers, and Mathlib import cache hits in a structured form. This creates a generate-verify-revise loop that continues until Lean itself reports verified.

The plugin reuses a persistent LSP process, so checks within the same session become significantly faster after the first call. It detects .olean cache hits for precise Mathlib sub-modules and triggers only a one-time user-authorized minimal build when a module is missing; it never runs a full compilation or modifies the local Mathlib directory. Additional tools include tactic state formatting, a low-level LSP debug channel, and an optional natural-language problem formalization Skill that helps the model clarify variables, quantifiers, and conclusions before writing any proof.

Ideal for researchers and developers working on theorem proving, algebra, or formal mathematics who use deepseek-harness or similar AI hosts and want the Lean compiler verdict, not model intuition, to be the sole success criterion.