lean4-harness-plugin

deepseek-harness 的 Lean 4 本地验证插件。 作者：ygw｜当前发布版本：0.1.1｜适用环境：Windows 11、Lean 4.26.0、Mathlib 4、deepseek-harness 0.1.3-alpha.2。

lean4-harness-plugin 不替模型“猜”证明是否正确。模型生成 Lean 4 源码后，插件会调用本地 Lean 验证器，并把真实结果、诊断位置、错误信息和导入缓存状态返回给模型。模型据此修改代码并再次检查，直至 Lean 明确通过。

当前已实现：

• 完整 Lean 4 源码验证；
• 常驻 Lean LSP 进程复用；
• 结构化错误、警告、行号和列号；
• 精确 Mathlib 模块的 .olean 缓存检查；
• 缺失精确 Mathlib 模块时的用户一次授权与受控最小构建；
• tactic state 格式化；
• 可选的自然语言数学题规约 Skill。

更详细的运行关系见 docs/architecture.md。

怎样使用

如果你已经打开 http://127.0.0.1:3080/，并且当前 Web Profile 已加载本插件，那么不需要手动启动 Lean，也不需要填写工具 JSON。只需新建对话，给模型数学题，并明确要求它在完成前调用 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 可能需要几十秒到数分钟：Lean LSP 需要把所需的、已经存在于本机的 .olean 文件读入内存。这不是下载或全量重编译 Mathlib。之后同一 Web 服务中的验证会复用常驻进程，结果里的 reusedProcess 通常为 true，速度会明显提升。

Harness 如何加载和使用插件

本插件不需要复制到 deepseek-harness 的 packages/ 目录。它作为一个 DSH Bundle 被 Profile 安装和加载：

deepseek-harness Web Profile
        │
        │  安装 lean4-harness-plugin
        ▼
package.json 的 dsh.bundle 声明
        │
        ▼
cordis.patch.yml
        │  插入 lean4-harness-plugin/dsh
        ▼
dsh-plugin.js（Cordis 入口，apply(ctx)）
        │
        ├── 注册 lean_check
        ├── 注册 lean_repl_request
        ├── 注册 lean_format_tactic_state
        ├── 注入 Lean 验证提示
        └── 阻止模型直接执行危险的 Lake / Mathlib 操作
        │
        ▼
dist/index.js
        │
        ▼
LeanReplService + LeanFormatter
        │
        ▼
lean/ Lake 工作区 ──── D:/mathlib4 的本地 .olean 缓存

因此，deepseek-harness 是宿主，而 D:\lean4-harness-plugin 是 Lean 验证逻辑的唯一来源。以后修改插件时，只需重新构建本仓库并重启 Harness，不必在 Harness 源码中维护第二份 Lean 实现。

当前真实目录结构

以下是当前需要纳入版本控制的真实结构：

lean4-harness-plugin/
├── package.json                         # npm 包、DSH Bundle 声明、构建和测试脚本
├── package-lock.json                    # Node 依赖锁定
├── tsconfig.json                        # TypeScript 编译配置
├── cordis.patch.yml                     # Profile 配置层：加载 lean4-harness-plugin/dsh
├── dsh-plugin.js                        # 真正的 Cordis / DSH 运行时入口
├── README.md                            # 安装、使用、配置和排错说明（本文件）
├── AGENTS.md                            # 项目开发约定
│
├── docs/
│   └── architecture.md                  # 运行架构、边界和后续演进
│
├── lean/                               # 插件自己的 Lean 4 Lake 工作区
│   ├── lean-toolchain                  # 锁定 leanprover/lean4:v4.26.0
│   ├── lakefile.lean                   # Lake 配置；当前使用 D:/mathlib4
│   ├── lake-manifest.json              # Lake 依赖清单
│   ├── Lean4Harness.lean               # 插件 Lean 库入口
│   ├── Main.lean                       # 可手动验证的 Lean 示例
│   └── README.md                       # Lean 工作区单独说明
│
├── scripts/
│   ├── Initialize-LeanEnvironment.ps1  # 检查 Lean / Lake / Mathlib 环境
│   └── Install-LeanProblemFormalizerSkill.ps1
│                                        # 将可选 Skill 安装到指定 DSH_HOME
│
├── skills/
│   └── lean-problem-formalizer/
│       └── SKILL.md                    # 数学题 → Lean 验证任务规约 Skill
│
├── src/                                # 可独立复用的 TypeScript 验证核心
│   ├── index.ts                        # TypeScript 公共 API；不是 Cordis 入口
│   ├── services/
│   │   └── lean-repl.ts                # 常驻 LSP、导入检查、受控构建、清理
│   ├── types/
│   │   └── index.ts                    # 诊断、配置与导入检查类型
│   ├── utils/
│   │   ├── formatter.ts                # Lean 诊断和 tactic state 格式化
│   │   └── object-utils.ts             # 统一空值判断工具
│   └── tests/
│       ├── formatter.test.ts           # 格式化测试
│       └── lean-repl.test.ts           # 真实常驻 Lean LSP 回归测试
│
└── tests/
    └── dsh-plugin.test.mjs             # Bundle 入口和工具契约测试

dist/ 是一个例外：它由 npm run build 从 src/ 生成，但经过构建和测试后的版本会提交到 Git，作为固定 Commit 的受控运行产物。DSH STORE 不执行第三方的 install、prepare、build 或 test 脚本；因此不能依赖安装期构建来取得 dist/index.js。开发者修改 TypeScript 后必须重新构建、测试并一并提交对应的 dist/ 变更。 dsh-plugin.js 与 src/index.ts 的职责不同：前者由 deepseek-harness 加载，负责 Cordis 生命周期和模型工具；后者是可被其他 TypeScript 程序调用的验证核心 API。普通 Web 使用者只需要前者。

前置条件

必需项	当前项目要求	检查方式
操作系统	Windows 11；文档命令均为 PowerShell	Get-ComputerInfo
Node.js	>= 22.19.0	node --version
pnpm	deepseek-harness 使用的包管理器	pnpm --version
deepseek-harness	当前经过验证的版本：0.1.3-alpha.2	查看 Harness 根目录 package.json
Lean	leanprover/lean4:v4.26.0，由 elan 安装	lean --version
Lake	与 Lean 同一工具链	lake --version
Mathlib 4	与 Lean 4.26.0 匹配，且已有本地 .olean	Test-Path 'D:\mathlib4\Mathlib'

当前 lean/lakefile.lean 明确写有：

require mathlib from "D:/mathlib4"

所以插件不会在安装时下载 Mathlib库，也不会把 Mathlib库打包上传到 GitHub。当前电脑直接使用 D:\mathlib4 即可；另一台电脑若将 Mathlib 放在其他位置，必须先准备与 Lean 4.26.0 匹配的 Mathlib库，然后修改 lean/lakefile.lean 中的路径并重新构建插件。仅修改 Bundle 的 mathlibRoot 配置不能改变 Lake 的依赖路径。

可以先执行以下环境检查：

Set-Location D:\lean4-harness-plugin
.\scripts\Initialize-LeanEnvironment.ps1

该脚本只构建插件自己的小型 Lake 工作区；不会执行 lake update，不会下载依赖，也不会全量重编译 D:\mathlib4。

首次安装到 deepseek-harness

以下步骤适用于新建或重新配置一个独立 Harness Profile。

1. 构建并测试插件

Set-Location D:\lean4-harness-plugin
npm install
npm run build
npm test
npm run verify:distribution

npm test 包含真实常驻 Lean LSP 回归测试，首次可能耗时约一分钟。它读取本地 .olean，不会重新下载或全量构建 Mathlib。

2. 将本地仓库链接到 Web Profile

在 Harness 源码目录运行：

Set-Location D:\deepseek-harness\deepseek-harness
$env:DSH_HOME = 'D:\lean4-harness-plugin\.dsh-lean4-plugin-test'

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

第二条命令的结果应出现：

# == lean4-harness-plugin
- id: lean4-harness-plugin
  name: lean4-harness-plugin/dsh

这说明 Harness 已读取 cordis.patch.yml，并会从本仓库加载 dsh-plugin.js。如果同一 Profile 中仍出现旧的 dsh-experimental-lean4-profile，请先移除旧层；一个 Profile 中不应保留两套同名 lean_check。

3. 启动 Web UI

仍在同一个 PowerShell 窗口运行：

pnpm dsh --profile web --no-open --port 3080

终端会打印带访问令牌的本地地址。令牌是本机访问凭证，不要发布到 GitHub、截图或聊天记录中。当前会话已经为你启动了同一个 Profile，因此现在可直接继续使用 http://127.0.0.1:3080/。

4. 在 Web 对话中验证

新建对话，把数学题交给模型，并在题目末尾加上：

- 写出完整 Lean 4 源码和最小必要的 Mathlib 子模块导入；
- 不要使用顶层 import Mathlib；
- 第一版代码后必须调用 lean_check；
- 如果验证失败，依据 Lean 诊断修改并继续调用 lean_check；
- 只有 verified 才能宣布完成。

模型会自行生成 lean_check 的参数并调用工具。用户不需要在 Web 页面中手动填写 source 或文件名。

推荐的 Mathlib 测试题

为了确认模型使用的是 Mathlib 子模块而不是只验证纯 Lean 语法，可将下题交给模型。这里不提供证明代码：

请使用 Lean 4 和 Mathlib 证明：对任意实数 x，sin (-x) = -sin x。

请自行选择最小必要的 Mathlib 子模块；不要使用 import Mathlib。
写出完整源码，并在宣布证明完成前调用 lean_check。
若检查失败，请依据诊断修改代码并继续验证。

在当前已完整恢复缓存的 D:\mathlib4 环境中，三角函数所需精确模块应直接命中 .olean 缓存，不应请求补齐授权。

模型工具说明

普通用户主要关注 lean_check。另外两个工具服务于高级调试或后续扩展。

工具	建议调用者	输入	返回 / 用途
lean_check	模型在每次完整源码生成或修改后调用	source、file_name	验证结果、诊断、导入缓存检查和可选构建结果。
lean_repl_request	高级 LSP / JSON 行调试流程	id、method、可选 params	原样转发 Lean LSP 或 JSON 行 REPL 请求；普通证明不需要。
lean_format_tactic_state	模型或调试工具	tactic_state	返回结构化目标和 Markdown。

注意：DSH Bundle 中的 lean_check 使用下划线参数 file_name。独立 TypeScript API 使用 fileName；两种接口不要混用。

典型结果包含：

success: true / false                 # Lean 是否没有阻断性错误
status: verified / invalid / ...      # 稳定状态
reusedProcess: false / true           # 是否复用了常驻 Lean LSP
diagnostics: [...]                    # 文件、行、列、严重级别与消息
importInspection:                     # 显式 import 的本地缓存检查
  cachedImports: [...]
  missingImports: [...]
  buildTargets: [...]

状态	含义	下一步
verified	Lean 无错误通过	可以说明证明已验证。
verified_with_warnings	Lean 通过但有警告	可以说明通过，同时查看警告。
invalid	解析、类型检查或证明失败	根据 diagnostics 修改后重试。
configuration_error	工作区、导入或环境配置不正确	检查 Mathlib 路径、Lean 版本和精确导入。
authorization_rejected	用户拒绝构建缺失模块	不修改缓存；可换用可用模块或稍后批准。
authorization_cancelled	授权窗口被取消	重新发起验证或换用缓存模块。
authorization_unavailable	宿主没有可用授权通道	检查 Profile 是否提供用户授权服务。
build_failed	已授权精确模块构建失败	查看构建输出，检查 Lake / Mathlib 环境。

Mathlib 缓存、授权与安全边界

普通验证只读取本地缓存：

模型源码
   │
   ▼
检查每个精确 import 是否已有 .olean
   │
   ├── 全部命中 → 常驻 Lean LSP 验证
   │
   └── 缺失 Mathlib.* → 显示精确模块并请求用户一次授权
                         │
                         ├── 拒绝 / 取消 → 不构建，返回状态
                         └── 批准 → 仅构建该模块 → 重启 LSP → 再验证原源码

插件不会因为模型请求而执行：

• lake update；
• lake clean；
• lake exe；
• Mathlib 全量构建；
• 直接修改 D:\mathlib4；
• 将模型或未来 LeanCopilot 的建议视为已验证证明。

模型直接尝试执行上述 Lake 命令或写入受保护 Mathlib 目录时，会被最终工具守卫拒绝。顶层聚合导入 import Mathlib 不会被当成可自动补齐的精确模块；请始终选择具体的 Mathlib.* 子模块。

Bundle 配置

默认配置位于 cordis.patch.yml：

- insert:
    - id: lean4-harness-plugin
      name: 'lean4-harness-plugin/dsh'
      config:
        mathlibRoot: 'D:/mathlib4'
        requestTimeoutMs: 600000
        buildTimeoutMs: 600000
        prewarm: false
        prewarmSource: |
          import Mathlib.Data.Nat.Basic

字段	默认值	作用
workspaceRoot	插件包内的 lean/	Lake 工作区路径。
mathlibRoot	D:/mathlib4	Mathlib 写入防护范围；不替代 lakefile.lean 的依赖路径。
lakeCommand	lake	Lake 命令或绝对路径。
leanCommand	lean	Lean 命令或绝对路径。
requestTimeoutMs	600000	前台启动、验证和诊断最大时长，单位毫秒。
buildTimeoutMs	600000	已授权精确模块构建最大时长，单位毫秒。
prewarm	false	true 时 Web 启动后预热可信导入；false 时首个 lean_check 延迟启动。
prewarmTimeoutMs	90000	后台预热最大时长，单位毫秒。
prewarmSource	import Mathlib.Data.Nat.Basic	预热使用的可信源码。
maxResultChars	16000	返回给模型的 stderr / 构建输出最大字符数。

例如，希望明确固定路径并开启预热时，可在 config 中补充：

workspaceRoot: 'D:/lean4-harness-plugin/lean'
mathlibRoot: 'D:/mathlib4'
lakeCommand: 'lake'
leanCommand: 'lean'
prewarm: true
prewarmTimeoutMs: 90000

修改 cordis.patch.yml 或 package.json 后，需要重新安装 Bundle：

Set-Location D:\deepseek-harness\deepseek-harness
$env:DSH_HOME = 'D:\lean4-harness-plugin\.dsh-lean4-plugin-test'
pnpm dsh plugin --profile web remove lean4-harness-plugin
pnpm dsh plugin --profile web add 'link:D:\lean4-harness-plugin'
pnpm dsh --profile web --dump-config

可选：安装数学题规约 Skill

lean-problem-formalizer 不写证明，也不自动验证。它把自然语言数学题整理成适合交给 Lean 模型的任务说明：明确变量类型、量词、定义、前提、结论、歧义处置、最小导入约束与验证要求。

安装到当前隔离 Profile：

Set-Location D:\lean4-harness-plugin
.\scripts\Install-LeanProblemFormalizerSkill.ps1 -DshHome 'D:\lean4-harness-plugin\.dsh-lean4-plugin-test'

之后在新的 Web 对话中说：

请使用 lean-problem-formalizer，把下面的数学题整理成 Lean 4 证明与验证任务。

Skill 只规约题意；模型生成 Lean 源码后仍必须调用 lean_check。

发布状态

• GitHub 仓库：Cosmicwanderer1/lean4-harness-plugin
• 当前 Bundle 已在 deepseek-harness 0.1.3-alpha.2 的真实独立 Profile 中启动验证。
• DSH 仍处于预览期。升级 Harness 后，请先执行 --dump-config，再使用一个小型 Lean 定理实际调用 lean_check 回归验证。
• Lean 诊断是唯一的成功依据。