lean4-harness-plugin

用 AI 撰写 Lean 4 形式化证明时，最大的风险是模型生成的代码没有任何真实验证反馈——它只能靠语义猜测来判断证明是否正确，而形式化数学恰恰不接受猜测。lean4-harness-plugin 在 deepseek-harness 中补上这一环节：模型每次生成或修改 Lean 源码后，插件直接调用本地 Lean LSP 进程进行完整编译验证，将真实的通过状态、错误诊断、行号列号以及 Mathlib 导入缓存命中情况结构化地返回给模型，形成生成、验证、修改的闭环，直到 Lean 明确给出 verified 为止。

插件复用常驻 LSP 进程，首次验证后同一会话中的后续检查速度显著提升；对精确 Mathlib 子模块的 .olean 缓存做命中检测，缺失时仅触发用户一次授权的最小构建，绝不执行全量编译或直接修改本地 Mathlib 目录。此外还提供 tactic state 格式化、低层 LSP 调试通道等辅助工具，以及可选的自然语言数学题规约 Skill，帮助模型在动手写证明前先厘清变量、量词与结论。

适合正在用 deepseek-harness 或同类 AI 宿主处理定理证明、代数学、形式化数学任务的研究者与开发者——凡是希望模型不再凭直觉输出 Lean 代码、而是以 Lean 编译器判定为唯一成功依据的场景，都可以直接接入。