前言¶
在构建依赖 Lean 4 和 Mathlib 的智能体应用时，直接让模型输出代码而不进行本地验证，往往会导致生成的证明无法通过编译。lean4-harness-plugin 是 DeepSeek Harness（DSH）的一个插件，它将本地的 Lean 4 验证器与 Web Profile 中的智能体连接起来。模型生成 Lean 4 源码后，插件会调用本地 Lean 验证器，并将验证结果（包括错误信息、行号、列号和缓存状态）返回给模型。模型据此修改代码并再次检查，直至 Lean 明确通过。
核心功能¶
插件提供以下核心能力：
- 完整 Lean 4 源码验证
- 常驻 Lean LSP 进程复用，避免重复启动
- 结构化错误、警告、行号和列号返回
- 精确 Mathlib 模块的 .olean 缓存检查
- 缺失 Mathlib 模块时的用户一次授权与受控最小构建
- tactic state 格式化
- 工具：
lean_check、lean_repl_request、lean_format_tactic_state
前置条件¶
安装前需确认环境满足以下要求：
- 操作系统：仅支持 Windows 11
- Node.js：>= 22.19.0
- DeepSeek Harness：0.1.3-alpha.2
- Lean：leanprover/lean4:v4.26.0
- Mathlib 4：需安装在本地路径
D:\mathlib4，且包含匹配版本的 .olean 缓存文件
安装与启用¶
插件通过 DSH Bundle 机制加载，不需要复制到 Harness 的 packages/ 目录。
使用 link: 语法将本地仓库链接到 Web Profile：
pnpm dsh plugin --profile web add 'link:D:\\lean4-harness-plugin'
执行上述命令后，在 Web Profile 的配置中应能看到 lean4-harness-plugin 的声明。
典型用法¶
新建对话，给模型数学题，并明确要求它在完成前调用 lean_check。
可以将以下测试要求交给模型：
请使用 Lean 4 和 Mathlib 证明自然数加法满足：1 + 2 = 2 + 1。
要求：
1. 自行写出完整 Lean 4 源码；
2. 自行选择最小必要的 Mathlib 子模块，不要使用 import Mathlib；
3. 生成第一版代码后，必须调用 lean_check；
4. 若 lean_check 返回错误，请依据错误信息修改并继续验证；
5. 只有 lean_check 返回 verified 或 verified_with_warnings 后，才能说明证明完成。
性能说明：第一次 lean_check 可能需要几十秒到数分钟，这主要用于将本地已存在的 .olean 文件读入内存。同一 Web 服务中的后续验证会复用常驻 Lean LSP 进程，结果里的 reusedProcess 通常为 true，速度会明显提升。
注意事项¶
- 插件不替模型“猜”证明是否正确，完全依赖本地 Lean 验证器。
- 插件依赖本地 Mathlib (
D:\mathlib4)，不会在安装时下载。 - 必须使用
link:语法将本地仓库链接到 Web Profile，而不是直接引用远程仓库。 - 仅支持 Windows 11。
