lean4

Lean 4 定理证明

在编辑 Lean 4 证明、调试 Lean 构建、用 Lean 形式化数学或学习 Lean 4 概念时，请使用此技能。它优先采用基于 LSP 的检查和 mathlib 搜索，并提供用于分析 sorry、检查公理和解析错误的脚本化基础工具。

核心原则

先搜索，再证明。 mathlib 中已经包含许多数学事实。编写 tactic 前，请先全面搜索。

逐步构建。 Lean 的类型检查器就是你的测试套件——如果代码编译通过、没有 sorry，且只使用标准公理，那么证明就是可靠的。

尊重范围。 遵循用户的偏好：补全一个 sorry、它的传递依赖、文件中的所有 sorry，或所有内容。如不明确，请询问。

Lean 文件每行宽度使用 100 个字符。 不要按 80 个字符换行——Lean 和 mathlib 的惯例是 100 个字符。如果一行不超过 100 个字符，就保持单行。超过 100 个字符时的换行策略请参阅 mathlib-style。

快速检查 mathlib 风格。 对于常规数学 lambda，请写 fun x ↦ ...（\mapsto），而不是 fun x => ...。在 match/do 分支和元编程回调惯用写法中使用 =>。tactic 证明优先使用 show P by tac；只有项证明才使用 show P from term。请参阅 mathlib-style。

保留命题和签名——它们是文件的契约。 除非用户明确要求修改，否则定理/引理命题和类型签名不可更改；更改它们可能会破坏调用方，或改变正在证明的定理。如果证明似乎需要更改命题或添加自定义公理，请先停下并讨论，因为这会改变契约或证明的信任基础。例外：在综合包装器（/lean4:formalize、/lean4:autoformalize）中，会话生成的声明可根据外层循环的命题安全规则重新起草；请参阅 cycle-engine.md。

文档字符串的适用范围取决于工作流。 现有文档字符串属于 API。默认规则是规则 A——任何会修改现有声明的工作流都应遵循此规则，除非用户明确要求修改文档字符串：

模式	可执行操作	边界
A — 编辑现有声明（例如 /lean4:prove、sorry-filler-deep、代码精简、重构，以及任何编辑现有声明的 Agent）	调整证明体中的行内注释	绝不重写现有文档字符串——只有用户明确要求时才可重写
B — 审查（/lean4:review）	指出薄弱或缺失的文档字符串，并在报告中提出替换文本	只读——绝不修改文件
C — 新文件/新声明生成（/lean4:draft、/lean4:formalize、/lean4:autoformalize）	为其新建的文件或声明生成模块/声明文档字符串	现有文档字符串仍受规则 A 约束

每条命令的策略见其文档。文档字符串规则适用于每个项目；当 mathlib Template Gate 选择 mathlib 文件头时，规则 C 会填写其模块文档字符串位置——规则 C 不会选择或重新定义模板。

命令

命令	用途
/lean4:draft	根据非形式化论述起草 Lean 声明骨架
/lean4:formalize	交互式形式化——起草并在引导下证明
/lean4:autoformalize	根据非形式化来源自主完成端到端形式化
/lean4:prove	通过明确的检查点，逐周期引导定理证明
/lean4:autoprove	通过明确的停止预算，自主进行多周期定理证明
/lean4:disprove	在引导下搜索反例，并进行有证书的反驳
/lean4:checkpoint	通过安全的提交检查点保存进度
/lean4:review	只读审查 Lean 证明
/lean4:refactor	利用 mathlib、提取辅助项并简化证明策略
/lean4:golf	提升 Lean 证明的直接性、清晰度、性能和简洁性
/lean4:learn	交互式教学和 mathlib 探索
/lean4:diagnose	诊断、清理和迁移帮助

/lean4:* 名称是原生插件的命令别名，也作为本文档中稳定的工作流名称。在未注册命令的宿主环境中（仅安装技能或便携式安装），请使用宿主通常采用的语法调用 lean4 技能，并指定工作流名称，例如：“对 Foo.lean:42 使用引导式 prove 工作流。”

此插件附带一个与宿主无关的解析器（lib/command_args/），用于处理七个参数较多命令（draft、learn、formalize、autoformalize、prove、autoprove、disprove）中可由解析器判定的启动规则。这些命令中有少量已记录的启动规则依赖运行时上下文（仓库级搜索、交互式提示），会在读取解析器输出后由命令应用。其他命令（checkpoint、review、refactor、golf、diagnose）仍由模型解析。 当宿主适配器安装 UserPromptSubmit 钩子时，对于匹配上述七个命令之一的 /lean4:* 提示，解析器会在模型看到提示之前运行，将 validated-invocation 块注入上下文，并在钩子层拒绝无效调用；其他命令的调用则不作修改地通过。未安装钩子的宿主会依据共享的 command-invocation.md 契约，回退到由模型解析启动参数。 命令始终会告知解析后的输入，在开始工作前拒绝无效的启动配置，并将 --max-total-runtime 等墙钟时间预算视为尽力而为。

应该使用哪个命令？

情况	命令
起草 Lean 骨架（默认生成骨架）	/lean4:draft
交互式起草并证明	/lean4:formalize
填补 sorry（交互式）	/lean4:prove
填补 sorry（无人值守）	/lean4:autoprove
搜索反例以反驳论述	/lean4:disprove
保存点（逐文件构建和项目构建、尽力而为的公理扫描、提交）	/lean4:checkpoint
质量检查（只读）	/lean4:review
简化证明策略（利用 mathlib、辅助项）	/lean4:refactor
优化已编译的证明	/lean4:golf
初次接触此项目／探索项目	/lean4:learn --mode=repo
围绕某个主题浏览 mathlib	/lean4:learn --mode=mathlib
遇到问题	/lean4:diagnose
无人值守地端到端完成形式化并证明	/lean4:autoformalize --source=... --claim-select=first --out=...

贡献（lean4-contribute 插件）

如果已安装 lean4-contribute 插件，你可以在自然的停顿处建议使用以下命令。规则：

• 先建议，绝不在未收到提示时调用。 提出一个简短问题；不要启动命令流程。
• 只有在当前对话中用户明确同意后，才能调用。 沉默、转移话题或含蓄地表达沮丧都不算同意。
• 每个话题每次会话最多建议一次，除非用户主动参与。
• 绝不要在证明过程中建议。 等待自然的停顿。

情况	建议
问题似乎出在 lean4-skills 本身（命令行为不正确、文档相互矛盾、lint 故障、保护措施不当、插件 UX 令人困惑）——而非普通的 Lean/mathlib/用户证明问题	“这看起来像是 lean4-skills 的 bug。要我起草一份 bug 报告吗？” → /lean4-contribute:bug-report
用户想要插件不支持的工作流、表示某个命令应该有不同的行为，或由于缺少功能而不得不建议笨拙的手动步骤	“这看起来像是插件工作流的缺口。要我起草一份功能请求吗？” → /lean4-contribute:feature-request
结果似乎对当前任务之外的场景也有用：策略选择启发式、mathlib 搜索模式、反模式、具有明确启示的文档缺口——而非一次性的定理事实或私有仓库细节	“这似乎对当前任务之外的场景也有用。要我起草一份可分享的经验吗？” → /lean4-contribute:share-insight

如果未安装插件，且用户明显遇到了 lean4-skills bug、工作流缺口或可复用的经验（标准同上——不包括普通 Lean/mathlib 问题），你可以建议一次安装：

• 每次会话最多建议一次。如果用户拒绝、忽略或转移话题，不要重复建议。
• 绝不要在证明过程中或正在进行的调试过程中建议。
• 只用一句简短的话，不要推销：“如果你愿意，可以安装 lean4-contribute 插件，我就能在这里帮你起草报告。” 设置说明请参阅 lean4-contribute README。

典型工作流

┌─ Entry points (pick one) ──────────────────────────────────────────────────────────┐
│ /lean4:draft              Skeleton by default (--mode=attempt for shallow proof)   │
│ /lean4:formalize          Interactive: draft + guided proving                      │
│ /lean4:autoformalize      Autonomous: draft + autonomous proving                   │
└────────────────────────────────────────────────────────────────────────────────────┘
        ↓ (if sorries remain)
/lean4:prove / autoprove    Proof engines (sorry filling, no header edits)
        ↓
/lean4:refactor            Leverage mathlib, extract helpers (optional)
        ↓
/lean4:golf                Improve proofs (optional)
        ↓
/lean4:checkpoint          Save point (per-file + project build)

随时使用 /lean4:learn 探索仓库结构或浏览 mathlib。三个入口：/lean4:draft 用于生成骨架，/lean4:formalize 用于交互式综合（起草 + 引导证明），/lean4:autoformalize 用于无人值守地将源代码转换为证明。

反证分支： 当目标是反驳某个陈述而非证明它时，使用 /lean4:disprove <target>。该命令始终采用交互模式；它会运行一个 6 阶段循环（规划 → 工作 → 检查点 → 审查 → 累积 → 继续/停止），其中第 1 阶段会生成动态的 Step 0 / Step 1 / Step 2 菜单，并以累积的证据为基础（第 5 阶段 — 累积 — 取代 prove 的 Replan）。每轮循环都会针对同一目标进行一次范围逐步扩大的搜索。仅追加内容——它会在原有的 sorry 旁添加一个 T_counterexample 定理，绝不重写原始声明。需要 Python 3.11+（注册表加载器）。参见 disprove-engine.md，包括其中的 Implementation Status 表（区分确定性、模型介导和延期的实现）。

注意：

• /lean4:prove 会在每轮循环前询问；/lean4:autoprove 会自主循环，并设有明确的停止预算
• 两者都会按配置的间隔触发 /lean4:review（--review-every）
• 运行审查时（通过 --review-every），审查会作为关卡：审查 → 重新规划 → 继续。在 prove 中，重新规划需要用户批准；在 autoprove 中，重新规划后会自动继续
• 审查支持 --mode=batch（默认）或 --mode=stuck（分诊）；审查始终为只读
• /lean4:autoformalize 将 draft+autoprove 封装为单个命令（源代码 → 声明 → 骨架 → 证明）；取代 autoprove --formalize=auto
• 证明引擎（prove/autoprove）绝不修改声明头部（头部围栏）
• /lean4:disprove 仅当 Lean 对否定式进行类型检查时才报告 REFUTED；否则报告 WITNESS_UNCERTIFIED 或 INCONCLUSIVE
• 如果遇到环境问题，运行 /lean4:diagnose 进行诊断

LSP 工具（首选）

通过 Lean LSP MCP 提供亚秒级反馈和搜索工具（LeanSearch、Loogle、LeanFinder）：

lean_goal(file, line)                           # See exact goal
lean_hover_info(file, line, col)                # Understand types
lean_local_search("keyword")                    # Fast local + mathlib (unlimited)
lean_leanfinder("goal or query")                # Semantic, goal-aware (10/30s)
lean_leansearch("natural language")             # Semantic search (3/30s)
lean_loogle("?a → ?b → _")                      # Type-pattern (unlimited if local mode)
lean_hammer_premise(file, line, col)            # Premise suggestions for simp/aesop/grind (3/30s)
lean_state_search(file, line, col)              # Goal-conditioned lemma search (3/30s)
lean_multi_attempt(file, line, snippets=[...])  # Test multiple tactics
lean_diagnostic_messages(file)                  # Per-file error/warning check
lean_code_actions(file, line)                   # Resolve "Try this" suggestions to edits

lean_run_code 用于隔离的临时实验，不能替代通过 lean_goal/lean_multi_attempt/lean_diagnostic_messages 检查实时证明状态。当问题依赖实际文件上下文时，优先使用实时文件工具。

功能

功能	必需	检查方式	后备方案
Lean / Lake	是	lean --version、lake --version	无——运行 /lean4:diagnose
Python 3	是（脚本）	python3 --version 或持久化的 $LEAN4_PYTHON_BIN	脚本依赖型操作无后备方案
辅助运行时路径	是（脚本）	可信的 Codex bin_dir/scripts_dir，或持久化的 $LEAN4_SCRIPTS	使用诊断工作流；若问题未解决，则仅使用 LSP
Lean LSP MCP	否	尝试对任意 .lean 文件调用 lean_goal	脚本 + lake env lean（仅文件级）
lean_run_code	否	尝试调用	对临时文件运行 lake env lean
lean_code_actions	否	尝试调用	手动应用“Try this”
子 Agent 派发	否	取决于宿主	在主线程中执行工作
斜杠命令	否	取决于宿主	直接遵循技能说明

运行配置

该技能会根据可用功能进行适配。通过检查上述功能确定你的配置，然后遵循相应的指导。

运行时路径解析

按以下顺序解析辅助运行时：

1. 受信任的原生 Codex 插件： SessionStart 上下文包含 lean4_plugin_runtime=codex、绝对的 bin_dir / scripts_dir 路径， 以及 shell_env_persistent=false。将这些字面绝对路径替换到辅助命令中。 它们是上下文值，不是 shell 变量：调用 /absolute/bin/lean4-skills-…，绝不要使用 $bin_dir/…，也不要指望 PATH 中存在不带路径的包装器。
2. 持久环境： 使用 $LEAN4_PLUGIN_ROOT、$LEAN4_SCRIPTS、 $LEAN4_REFS，以及已确认在 PATH 中的包装器。
3. 没有辅助运行时： 保留在由 LSP 支持的核心技能中，并跳过依赖脚本的步骤， 直到修复或升级安装。

当 shell 变量未设置时，不要输出 $LEAN4_BIN/... 或 $LEAN4_SCRIPTS/... 命令。 受信任的 Codex 绝对路径是完整的替代方案，并不表示持久变量存在。

full（所有功能）

MCP + 子 Agent + 命令。完整工作流，包含实时目标检查、策略测试和并行子 Agent 派发（要求每个 Agent 负责的文件集互不重叠，或使用独立的工作树）。子 Agent 会根据 cycle-engine.md § 派发前上下文 获取预先收集的 MCP 上下文。如果 lean_run_code 不可用，请使用 /tmp 临时文件 和 lake env lean 进行独立实验。

mcp_main_only（MCP 可用，不派发子 Agent）

MCP 在主线程中可用。直接完成所有证明工作——不要委派给子 Agent。所有 cycle-engine 阶段均在线程内执行。如果 lean_run_code 不可用，请使用 /tmp 临时文件和 lake env lean 进行独立实验。

scripts_only（无 MCP，无子 Agent）

使用已解析的辅助运行时（原生 Codex 下的 scripts_dir， 持久环境下的 $LEAN4_SCRIPTS）进行搜索，并使用 lake env lean / lake build 进行验证。此模式的主要限制：

• 无法实时检查目标——lean_goal 不可用；可以读取文件并检查编译输出，但无法查看特定行上的证明状态
• 无法测试策略——lean_multi_attempt 不可用；必须通过编译文件（lake env lean）来验证编辑
• 无法获取实时诊断信息——lean_diagnostic_messages 不可用；使用 lake env lean <file>（从项目根目录运行）查看编译错误，但反馈针对整个文件，而不是具体行
• 搜索基于脚本——lean4-skills-smart-search 会取代 LSP 搜索工具

此模式适用于简单的证明，但比由 MCP 支持的工作流慢得多，精确度也低得多。

review_only（只读，不编辑）

读取证明状态并评估质量。不编辑、不提交、不派发子 Agent。

文件处理规则

临时工作阶梯（按优先顺序）：

1. 实时文件 + MCP 工具（lean_goal、lean_multi_attempt、lean_diagnostic_messages）
2. 使用 lean_run_code 进行独立实验
3. 仅当 lean_run_code 不可用且实验不得触及实时文件时，才使用 /tmp 临时文件
4. 绝不要在仓库根目录创建临时文件

文件检查： 使用直接的文件读取和搜索工具检查源文件——例如在可用时使用 Read/Grep，或在 shell 中按行范围读取并使用 rg。不要仅为读取可直接访问的行而启动 Python 脚本、创建临时文件或使用 cat 管道；只有在直接读取/搜索工具无法妥善处理实际解析、转换或多文件分析时，才使用脚本。

暂存： 只暂存当前会话中修改过的文件。绝不要使用 git add -A 或宽泛的 glob 模式。提交前打印准确的暂存文件列表。

完整的临时工作偏好顺序请参阅 sorry-filling.md。

核心基元

脚本	用途	输出
sorry_analyzer.py	查找带上下文的 sorry	text（默认）、json、markdown、summary
check_axioms_inline.sh	尽力扫描公理（顶层声明）	text
smart_search.sh	多来源 mathlib 搜索	text
find_golfable.py	检测优化模式	JSON
find_usages.sh	查找声明的用法	text

用法： 由命令自动调用。详情请参阅 [references/]。

调用约定。 面向模型的首选形式：

• 对受支持的辅助脚本，使用 lean4-skills-* 包装器 （lean4-skills-sorry-analyzer、lean4-skills-check-axioms-inline、 lean4-skills-find-golfable、lean4-skills-find-exact-candidates、 lean4-skills-analyze-let-usage、lean4-skills-find-usages、 lean4-skills-search-mathlib、lean4-skills-smart-search、 lean4-skills-cycle-tracker、lean4-skills-disprove-artifact-txn、 lean4-skills-disprove-emit-artifact、lean4-skills-disprove-method-probe、 lean4-skills-disprove-target-profile、 lean4-skills-disprove-target-resolve、lean4-skills-file-baseline、 lean4-skills-project-context、 lean4-skills-checkpoint-mathlib-roots、 lean4-skills-validate-review-output、lean4-skills-run-store、 lean4-skills-run-persist）。在持久化环境中，这些是 PATH 上的裸命令。在可信的原生 Codex 插件中，在包装器名称前加上 SessionStart 提供的字面绝对 bin_dir 路径（例如 /installed/plugin/bin/lean4-skills-sorry-analyzer）。不要使用 $LEAN4_SCRIPTS、${LEAN4_PYTHON_BIN:-python3}、~ 或命令替换来定位包装后的可执行文件。对包装器进行常规输出捕获是可以的（例如 txn=$(lean4-skills-disprove-artifact-txn begin)）。这是沙盒主机可以静态加入允许列表的稳定调用接口。
• 仅报告的调用：向 lean4-skills-sorry-analyzer、lean4-skills-check-axioms-inline（以及通过环境变量回退方式调用的 unused_declarations.sh）添加 --report-only——发现问题时不以状态码 1 退出；实际错误仍以状态码 1 退出。不要在 /lean4:checkpoint 等门禁命令中使用。
• 保持 stderr 可见，用于 Lean 脚本调用（不要重定向到 /dev/null）。防护规则检测器可识别包装器和环境变量调用形式；无论哪种情况，屏蔽 stderr 都会被阻止。

兼容性回退（包装器不可用时）：

• 在可信的原生 Codex 下，使用 SessionStart 提供的字面绝对 bin_dir 路径；PATH 中没有裸命令是预期情况，并非故障。
• 对于持久化环境主机，如果 PATH 上无法解析 lean4-skills-*，请修复文档所述的 $LEAN4_PLUGIN_ROOT/bin 设置；参见仓库的 INSTALLATION.md。
• 只有在最后不得已时，才对未包装脚本使用显式环境变量形式：bash "$LEAN4_SCRIPTS/script.sh" … 或 ${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/script.py" …。

如果既没有可信 Codex 绝对路径，也没有 $LEAN4_SCRIPTS，请运行诊断工作流（若已安装该命令，则运行 /lean4:diagnose）；仅安装技能时，请遵循仓库的 INSTALLATION.md。 解决问题之前，请仅使用 LSP。

自动化

/lean4:prove 和 /lean4:autoprove 可处理大多数任务：

• prove — 引导式，每个循环前都会询问。适用于交互式会话。
• autoprove — 自主式，在明确的停止预算内循环。适用于无人值守运行。

两者共享相同的循环引擎（规划 → 工作 → 检查点 → 审查 → 重新规划 → 继续／停止），并遵循 LSP 优先协议：LSP 工具是发现和搜索的规范方式；仅在 LSP 不可用或已用尽时才回退到脚本。编译器引导的修复仅用于升级处理，不是应对构建错误的首选方式。对于复杂证明，它们可能会委派给内部工作流，以深入填补 sorry（包含快照、回滚和范围预算）、修复证明或消除公理。无需直接调用这些工作流。

仅技能模式行为

在不调用命令的情况下编辑 .lean 文件时，该技能会运行一次有界处理：

• 通过 lean_goal/lean_diagnostic_messages 读取目标或错误

• 使用最多 2 个 LSP 工具搜索 mathlib（例如 lean_local_search + lean_leanfinder/lean_leansearch/lean_loogle）

• 尝试自动化策略级联

• 使用 lean_diagnostic_messages 验证（此模式下不运行项目门禁 lake build）

• 不循环、不深入升级、不进行多轮处理、不提交

• 如果某个目标在此轮处理中仍未解决，请在升级处理前遵循 references/sorry-filling.md 中的受阻目标分类循环

• 结束时给出建议：

  请让我运行引导式 prove 工作流，逐轮协助。 请让我运行自主式 autoprove 工作流，在停止保护机制下进行无人值守循环。

  （在已安装该插件命令的主机上，这些命令是 /lean4:prove 和 /lean4:autoprove。）

质量门禁

满足以下条件即表示证明完成：

• lake build 通过
• 约定范围内没有 sorry
• 仅使用标准公理（propext、Classical.choice、Quot.sound）
• 未经许可不更改陈述

验证阶梯：每次编辑后运行 lean_diagnostic_messages(file) → lake env lean <path/to/File.lean> 文件门禁（从项目根目录运行；仅针对已构建的导入项检查——跨文件编辑后使用 lake lean <path/to/File.lean>，见文件门禁范围）→ 仅以 lake build 作为项目门禁。参见 cycle-engine：构建目标策略。

常见修复

有关逐项错误的指导（类型不匹配、标识符未知、无法合成、超时等），请参见编译错误。

类型类模式

-- Local instance for this proof block: plain `have`/`let` already register a
-- class-typed local for synthesis in Lean 4
have : MeasurableSpace Ω := inferInstance
let inst : Fintype α := ⟨...⟩   -- `let` when the VALUE must stay visible (data)

-- Scoped instances (affects current section)
open scoped Topology MeasureTheory

haveI / letI 规则（Lean 4）： have 和 let 本身就会注册局部实例；haveI/letI 的区别仅在于将值内联到项中。在命题的策略证明中，这种内联可能不起作用（证明无关性），因此那里不需要 haveI/letI — Mathlib 的 haveI/letI linter 会标记它们。仅在实例值必须内联到数据中的定义里使用 letI。添加任何局部实例前，请先检查类型类合成是否已能成功（许多“提供该实例”的惯用写法早于对应的 Mathlib 实例）。

顺序很重要：先提供外层结构，再提供内层结构。

omit [Inst] in 会从后续声明中移除未使用的节实例。 将它放在声明文档字符串之前；如果放在文档字符串与 lemma/theorem 之间，Lean 会将其解析为独立的 omit 命令。

variable {α : Type*} [MeasurableSpace α]

omit [MeasurableSpace α] in
/-- doc -/
theorem foo : True := trivial

更多内容请参见领域模式。

自动化策略

按顺序尝试（首次成功后停止）： rfl → simp → ring → linarith → nlinarith → omega → exact? → apply? → grind → aesop

注意：exact?/apply? 会查询 mathlib（速度较慢）。grind 和 aesop 功能强大，但可能超时。有关交互式工作流、注解策略和 simproc 升级，请参阅 grind-tactic。

故障排查

如果 LSP 工具没有响应，请检查上面的运行配置文件。在 scripts_only 模式下，已解析的辅助运行时可提供搜索功能， lake env lean 可提供文件级编译反馈，但无法实时检查目标、 测试策略或获取行级诊断。如果没有可用的辅助运行时路径，请运行诊断工作流进行排查。

脚本环境检查：

# Trusted native Codex: use the absolute path from SessionStart.
/absolute/plugin/root/bin/lean4-skills-preflight --codex
# Persistent environment:
echo "$LEAN4_SCRIPTS"
command -v lean4-skills-sorry-analyzer
# One-pass discovery for troubleshooting (human-readable default text):
lean4-skills-sorry-analyzer . --report-only
# Structured output (optional): --format=json
# Counts only (optional): --format=summary

冷启动 / 新工作树：

• 新工作树，或刚运行过 lake clean？请先在该工作树中预热缓存，再进行首次实际构建。
• 使用项目的缓存命令：较新版本的 Lake 使用 lake cache get；项目仍使用 mathlib 缓存可执行文件时，使用 lake exe cache get。
• 如果 Lean LSP 尚未预热或首次使用时超时，请运行一次 lake build 以引导工作区。
• 完成引导后，恢复正常的验证流程： lean_diagnostic_messages(file) → lake env lean <path/to/File.lean>（从项目根目录运行；仅适用于已构建的导入，参见 文件门槛范围）→ 仅在检查点 / 最终门槛运行 lake build。
• 不要为另一个工作树的 .lake/build 创建符号链接；请改用 Lake 缓存 / 构件机制。

参考资料

循环引擎： cycle-engine — 共享的 prove/autoprove 逻辑（卡住、深度模式、证伪、安全性）

交接契约： handoff-contract — run-contract/v1 分派与交接记录，以及重新运行保护（若没有新证据，不要针对同一个 blocker_signature 重新启动相同模式；应转至 review --mode=stuck、formalize 或人工交接）

运行存储： run-store — run-store/v1，用于存储这些记录的基础机制（lean4-skills-run-store：不可变清单、仅追加日志、可丢弃的交接缓存；属于历史证据，绝非认证）。prove/autoprove --persist 会根据 cycle-engine § 运行持久化 (#82B)，通过 lean4-skills-run-persist 写入运行记录；根据 cycle-engine § 先前运行复用，通过 --prior-run (#82C) 复用先前运行；恢复 / 检查仍在 #82 中待定。

LSP 工具： lean-lsp-server（快速入门）、lean-lsp-tools-api（完整 API — grep ^## 查找工具名称）

搜索： mathlib-guide（搜索现有引理时阅读）、lean-phrasebook（数学 → Lean 翻译）

审查： mathlib-review-taxonomy（mathlib 审查者会要求什么 — 九类审查要点）

错误： compilation-errors（出现任何构建错误时先阅读）、instance-pollution（类型类冲突 — grep ## Sub- 查找模式）、compiler-guided-repair（仅用于升级处理的修复 — 不用于首轮修复）

策略： tactics-reference（策略查找 — grep ^### TacticName）、grind-tactic（SMT 风格自动化 — simp 无法完成证明时使用）、simp-reference（机制选择、simp 范式、@[simp] 卫生、simproc 编写）、tactic-patterns、calc-patterns 证明开发： proof-templates、proof-refactoring（28K — 按主题 grep）、proof-simplification（策略层面：mathlib 搜索、同余引理、辅助定义提取）、sorry-filling

优化： proof-golfing（包含安全规则、有界 LSP 引理替换、批量重写、反模式；必要时升级到 axiom-eliminator）、proof-golfing-patterns、performance-optimization（按症状 grep）、profiling-workflows（诊断缓慢的构建/证明）

领域： domain-patterns（25K — grep ## Area）、measure-theory（28K）、axiom-elimination

风格： mathlib-style、verso-docs（Verso 文档注释角色和修正）

自定义语法： lean4-custom-syntax（构建记号、宏、 elaborator 或 DSL 时阅读）、metaprogramming-patterns（MetaM/TacticM API — 可组合代码块、elaborator）、scaffold-dsl（可复制粘贴的 DSL 模板）、json-patterns（json% 语法 + ToJson）

质量： linter-authoring（项目专属的 linter 规则）、ffi-interop（FFI、@&、init、符号链接）

工作流： agent-workflows、subagent-workflows、command-examples、learn-pathways（意图分类、游戏路线、源代码处理）

内部机制： review-hook-schema、compiler-internals（属性、特化、流水线）