lean4
Compare original and translation side by side
🇺🇸
Original
English🇨🇳
Translation
ChineseLean 4 Theorem Proving
Lean 4 定理证明
Use this skill whenever you're editing Lean 4 proofs, debugging Lean builds, formalizing mathematics in Lean, or learning Lean 4 concepts. It prioritizes LSP-based inspection and mathlib search, with scripted primitives for sorry analysis, axiom checking, and error parsing.
当你编辑Lean 4证明、调试Lean构建、用Lean进行数学形式化，或学习Lean 4相关概念时，均可使用本技能。它优先基于LSP的检查和mathlib搜索，同时提供用于sorry分析、公理检查和错误解析的脚本原语。
Core Principles
核心原则
Search before prove. Many mathematical facts already exist in mathlib. Search exhaustively before writing tactics.
Build incrementally. Lean's type checker is your test suite—if it compiles with no sorries and standard axioms only, the proof is sound.
Respect scope. Follow the user's preference: fill one sorry, its transitive dependencies, all sorries in a file, or everything. Ask if unclear.
Use 100-character line width for Lean files. Do not wrap lines at 80 characters — Lean and mathlib convention is 100. If a line fits within 100 characters, keep it on one line. See mathlib-style for breaking strategies when lines exceed 100.
Never change statements or add axioms without explicit permission. Theorem/lemma statements, type signatures, and docstrings are off-limits unless the user requests changes. Inline comments may be adjusted; docstrings may not (they're part of the API). Custom axioms require explicit approval—if a proof seems to need one, stop and discuss. Exception: within synthesis wrappers (, ), session-generated declarations may be redrafted under the outer-loop statement-safety rules; see cycle-engine.md.
/lean4:formalize/lean4:autoformalize先搜索，再证明。许多数学结论已存在于mathlib中。在编写策略前，先进行全面搜索。
增量构建。Lean的类型检查器就是你的测试套件——如果代码编译通过且无sorry标记，仅使用标准公理，那么证明就是可靠的。
遵循范围。遵循用户的偏好：填充单个sorry标记、其传递依赖项、文件中所有sorry标记，或全部内容。如果不明确，请询问用户。
Lean文件使用100字符行宽。不要在80字符处换行——Lean和mathlib的约定是100字符。如果一行内容在100字符以内，保持单行。当行内容超过100字符时，可参考mathlib-style中的换行策略。
未经明确许可，请勿修改声明或添加公理。定理/引理声明、类型签名和文档字符串禁止修改，除非用户要求调整。可调整行内注释；但文档字符串不可修改（它们属于API的一部分）。自定义公理需要明确批准——如果证明似乎需要添加公理，请停止操作并与用户讨论。例外情况：在合成包装器（、）中，会话生成的声明可根据外层循环的声明安全规则重新起草；详情请查看cycle-engine.md。
/lean4:formalize/lean4:autoformalizeCommands
命令
| Command | Purpose |
|---|---|
| Draft Lean declaration skeletons from informal claims |
| Interactive formalization — drafting plus guided proving |
| Autonomous end-to-end formalization from informal sources |
| Guided cycle-by-cycle theorem proving with explicit checkpoints |
| Autonomous multi-cycle theorem proving with explicit stop budgets |
| Save progress with a safe commit checkpoint |
| Read-only code review of Lean proofs |
| Leverage mathlib, extract helpers, simplify proof strategies |
| Improve Lean proofs for directness, clarity, performance, and brevity |
| Interactive teaching and mathlib exploration |
| Diagnostics, cleanup, and migration help |
This plugin ships a host-agnostic parser () that covers the
parser-decidable startup rules of the six parameter-heavy commands (,
, , , , ). A small set of
documented startup rules in these commands depend on runtime context (repo-
level search, interactive prompting) and are applied by the command after
reading the parser's output. The other commands (, ,
, , ) remain model-parsed.
When a host adapter installs the hook, the parser runs
before the model sees a prompt matching one of the six covered
commands, injects a block into context, and rejects
invalid invocations at the hook level; invocations of the other commands pass
through unchanged. Hosts without the hook fall back to model-parsed startup
via the shared command-invocation.md
contract.
Commands always announce resolved inputs, reject invalid startup configs before
doing work, and treat wall-clock budgets like as
best-effort.
lib/command_args/draftlearnformalizeautoformalizeproveautoprovecheckpointreviewrefactorgolfdoctorUserPromptSubmit/lean4:*validated-invocation--max-total-runtime| 命令 | 用途 |
|---|---|
| 根据非形式化声明生成Lean声明框架 |
| 交互式形式化——生成框架加引导式证明 |
| 从非形式化来源自动完成端到端形式化 |
| 带明确检查点的循环式引导定理证明 |
| 带明确停止预算的自主多循环定理证明 |
| 通过安全提交检查点保存进度 |
| 对Lean证明进行只读代码审查 |
| 利用mathlib、提取辅助函数、简化证明策略 |
| 优化Lean证明，使其更直接、清晰、高效且简洁 |
| 交互式教学与mathlib探索 |
| 诊断、清理与迁移帮助 |
本插件提供一个与宿主无关的解析器（），覆盖六个参数密集型命令（、、、、、）的解析可判定启动规则。这些命令中有一小部分已文档化的启动规则依赖于运行时上下文（仓库级搜索、交互式提示），会在命令读取解析器输出后应用。其他命令（、、、、）仍由模型解析。
当宿主适配器安装钩子后，解析器会在模型看到匹配六个受支持命令之一的提示前运行，将块注入上下文，并在钩子级别拒绝无效调用；其他命令的调用则直接通过。未安装该钩子的宿主会回退到通过共享的command-invocation.md契约进行模型解析启动。
命令会始终宣布已解析的输入，在执行工作前拒绝无效的启动配置，并将等时钟预算视为尽力而为的约束。
lib/command_args/draftlearnformalizeautoformalizeproveautoprovecheckpointreviewrefactorgolfdoctorUserPromptSubmit/lean4:*validated-invocation--max-total-runtimeWhich Command?
如何选择命令？
| Situation | Command |
|---|---|
| Draft a Lean skeleton (skeleton by default) | |
| Draft + prove interactively | |
| Filling sorries (interactive) | |
| Filling sorries (unattended) | |
| Save point (per-file + project build, best-effort axiom scan, commit) | |
| Quality check (read-only) | |
| Simplify proof strategies (mathlib leverage, helpers) | |
| Optimizing compiled proofs | |
| New to this project / exploring | |
| Navigating mathlib for a topic | |
| Something not working | |
| Formalize + prove end-to-end (unattended) | |
| 场景 | 命令 |
|---|---|
| 生成Lean框架（默认生成框架） | |
| 交互式生成框架+证明 | |
| 填充sorry标记（交互式） | |
| 填充sorry标记（无人值守） | |
| 保存点（单文件+项目构建、尽力而为的公理扫描、提交） | |
| 质量检查（只读） | |
| 简化证明策略（利用mathlib、辅助函数） | |
| 优化已编译的证明 | |
| 新项目上手/探索 | |
| 针对某主题浏览mathlib | |
| 出现问题无法正常工作 | |
| 端到端形式化+证明（无人值守） | |
Contributing (lean4-contribute plugin)
贡献（lean4-contribute插件）
If the plugin is installed, you may suggest these commands at natural stopping points. Rules:
lean4-contribute- Suggest first, never invoke unprompted. Offer a one-line question; do not start the command flow.
- Only invoke after explicit user opt-in in the current conversation. Silence, topic change, or implicit frustration do not count as consent.
- At most once per topic per session unless the user engages.
- Never mid-proof. Wait for a natural stopping point.
| Situation | Suggest |
|---|---|
| Problem appears to be in lean4-skills itself (wrong command behavior, contradictory docs, broken lint, bad guardrail, confusing plugin UX) — not ordinary Lean/mathlib/user-proof problems | "This looks like a lean4-skills bug. Want me to draft a bug report?" → |
| User wants a workflow the plugin doesn't support, says a command should behave differently, or you must recommend awkward manual steps due to a missing feature | "This looks like a plugin workflow gap. Want me to draft a feature request?" → |
| Result seems reusable beyond the current task: tactic-selection heuristic, mathlib search pattern, anti-pattern, documentation gap with a clear lesson — not one-off theorem facts or private repo details | "That seems reusable beyond this task. Want me to draft a shareable insight?" → |
If the plugin is not installed and the user clearly hit a lean4-skills bug, workflow gap, or reusable insight (same criteria as above — not ordinary Lean/mathlib issues), you may offer the install hint once:
- At most once per session. Do not repeat if the user declined, ignored it, or moved on.
- Never mid-proof or during an active debugging loop.
- One short line, not a pitch: "If you want, install the plugin and I can draft that report for you here." See the lean4-contribute README for setup.
lean4-contribute
如果已安装插件，你可以在自然的停顿点建议使用以下命令。规则：
lean4-contribute- 先建议，切勿擅自调用。提供一行简短的询问；不要启动命令流程。
- 仅在当前对话中获得用户明确同意后调用。沉默、话题变更或隐含的不满均不视为同意。
- 每个会话每个主题最多建议一次，除非用户主动参与。
- 切勿在证明过程中建议。等待自然的停顿点。
| 场景 | 建议话术 |
|---|---|
| 问题似乎出在lean4-skills本身（命令行为错误、文档矛盾、检查规则失效、防护机制故障、插件UX混淆）——而非普通的Lean/mathlib/用户证明问题 | "这看起来是lean4-skills的bug。需要我帮你起草一份bug报告吗？" → |
| 用户需要插件不支持的工作流、认为命令应改变行为，或你因缺少功能而不得不推荐繁琐的手动步骤 | "这看起来是插件的工作流缺口。需要我帮你起草一份功能请求吗？" → |
| 结果似乎可在当前任务之外复用：策略选择启发式、mathlib搜索模式、反模式、有明确改进方向的文档缺口——而非一次性定理事实或私有仓库细节 | "这似乎在当前任务之外也有复用价值。需要我帮你起草一份可分享的见解吗？" → |
如果未安装该插件，且用户遇到的明显是lean4-skills的bug、工作流缺口或可复用见解（符合上述标准——而非普通Lean/mathlib问题），你可以提供一次安装提示：
- 每个会话最多一次。如果用户拒绝、忽略或转移话题，请勿重复。
- 切勿在证明过程中或活跃的调试循环中提示。
- 使用简短的一句话，而非推销："如果需要，你可以安装插件，我可以在这里帮你起草相关报告。" 安装步骤请查看lean4-contribute README。
lean4-contribute
Typical Workflow
典型工作流
┌─ 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)Use at any point to explore repo structure or navigate mathlib. Three entry points: for skeletons, for interactive synthesis (draft + guided proving), for unattended source-to-proof.
/lean4:learn/lean4:draft/lean4:formalize/lean4:autoformalizeNotes:
- asks before each cycle;
/lean4:proveloops autonomously with explicit stop budgets/lean4:autoprove - Both trigger at configured intervals (
/lean4:review)--review-every - When reviews run (via ), they act as gates: review → replan → continue. In prove, replan requires user approval; in autoprove, replan auto-continues
--review-every - Review supports (default) or
--mode=batch(triage); review is always read-only--mode=stuck - wraps draft+autoprove in a single command (source → claims → skeletons → proofs); replaces
/lean4:autoformalizeautoprove --formalize=auto - Proof engines (/
prove) never modify declaration headers (header fence)autoprove - If you hit environment issues, run to diagnose
/lean4:doctor
┌─ 入口点（选择其一） ──────────────────────────────────────────────────────────┐
│ /lean4:draft 默认生成框架（--mode=attempt用于浅度证明） │
│ /lean4:formalize 交互式：生成框架 + 引导式证明 │
│ /lean4:autoformalize 自主式：生成框架 + 自主证明 │
└────────────────────────────────────────────────────────────────────────────┘
↓（如果仍有sorry标记）
/lean4:prove / autoprove 证明引擎（填充sorry标记，不修改声明头）
↓
/lean4:refactor 利用mathlib、提取辅助函数（可选）
↓
/lean4:golf 优化证明（可选）
↓
/lean4:checkpoint 保存点（单文件+项目构建）在任何阶段都可以使用探索仓库结构或浏览mathlib。三个入口点：用于生成框架，用于交互式合成（生成框架+引导式证明），用于无人值守的从源到证明流程。
/lean4:learn/lean4:draft/lean4:formalize/lean4:autoformalize注意事项：
- 在每个循环前会询问用户；
/lean4:prove会按照明确的停止预算自主循环/lean4:autoprove - 两者都会按配置的间隔（）触发
--review-every/lean4:review - 当审查运行时（通过），它们会作为 gate：审查 → 重新规划 → 继续。在prove模式下，重新规划需要用户批准；在autoprove模式下，重新规划会自动继续
--review-every - 审查支持（默认）或
--mode=batch（分类处理）；审查始终为只读--mode=stuck - 将draft+autoprove包装为单个命令（源 → 声明 → 框架 → 证明）；替代
/lean4:autoformalizeautoprove --formalize=auto - 证明引擎（/
prove）永远不会修改声明头（声明头边界）autoprove - 如果遇到环境问题，运行进行诊断
/lean4:doctor
LSP Tools (Preferred)
LSP工具（优先使用）
Sub-second feedback and search tools (LeanSearch, Loogle, LeanFinder) via Lean LSP MCP:
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 editslean_run_codelean_goallean_multi_attemptlean_diagnostic_messages通过Lean LSP MCP提供亚秒级反馈和搜索工具（LeanSearch、Loogle、LeanFinder）：
lean_goal(file, line) # 查看精确目标
lean_hover_info(file, line, col) # 理解类型
lean_local_search("keyword") # 快速本地+mathlib搜索（无限制）
lean_leanfinder("goal or query") # 语义化、目标感知搜索（10/30秒）
lean_leansearch("natural language") # 语义化搜索（3/30秒）
lean_loogle("?a → ?b → _") # 类型模式搜索（本地模式下无限制）
lean_hammer_premise(file, line, col) # 为simp/aesop/grind提供前提建议（3/30秒）
lean_state_search(file, line, col) # 基于目标状态的引理搜索（3/30秒）
lean_multi_attempt(file, line, snippets=[...]) # 测试多种策略
lean_diagnostic_messages(file) # 单文件错误/警告检查
lean_code_actions(file, line) # 将"Try this"建议转换为编辑操作lean_run_codelean_goallean_multi_attemptlean_diagnostic_messagesCapabilities
能力要求
| Capability | Required | Check | Fallback |
|---|---|---|---|
| Lean / Lake | yes | | none — run |
| Python 3 | yes (scripts) | | none for script-dependent operations |
| yes (set by bootstrap) | | run |
| Lean LSP MCP | no | try | scripts + |
| no | try calling it | |
| no | try calling it | manual "Try this" application |
| Subagent dispatch | no | host-dependent | run work in main thread |
| Slash commands | no | host-dependent | follow skill instructions directly |
| 能力 | 必需 | 检查方式 | fallback方案 |
|---|---|---|---|
| Lean / Lake | 是 | | 无 — 运行 |
| Python 3 | 是（脚本运行） | 检查bootstrap设置的 | 依赖脚本的操作无法执行 |
| 是（由bootstrap设置） | | 运行 |
| Lean LSP MCP | 否 | 在任意 | 脚本 + |
| 否 | 尝试调用 | 在临时文件上使用 |
| 否 | 尝试调用 | 手动应用"Try this"建议 |
| 子代理调度 | 否 | 依赖宿主 | 在主线程中执行任务 |
| 斜杠命令 | 否 | 依赖宿主 | 直接遵循技能指令 |
Operating Profiles
运行配置文件
The skill adapts to what's available. Determine your profile by checking capabilities above, then follow the corresponding guidance.
技能会根据可用的能力进行适配。通过检查上述能力确定你的配置文件，然后遵循相应的指导。
full (all capabilities)
full（所有能力可用）
MCP + subagents + commands. Full workflow with live goal inspection, tactic testing, and parallel subagent dispatch (requires disjoint owned-file sets per agent, or separate worktrees). Subagents get pre-collected MCP context per cycle-engine.md § Pre-flight Context. If is unavailable, use scratch files with for isolated experiments.
lean_run_code/tmplake env leanMCP + 子代理 + 命令。支持完整工作流，包括实时目标检查、策略测试和并行子代理调度（要求每个代理拥有不重叠的文件集，或使用独立工作树）。子代理会获取预收集的MCP上下文，详情请查看cycle-engine.md § Pre-flight Context。如果不可用，使用临时文件和进行独立实验。
lean_run_code/tmplake env leanmcp_main_only (MCP available, no subagent dispatch)
mcp_main_only（MCP可用，无子代理调度）
MCP works in the main thread. Run all proof work directly — do not delegate to subagents. All cycle-engine phases execute in-thread. If is unavailable, use scratch files with for isolated experiments.
lean_run_code/tmplake env leanMCP在主线程中工作。直接运行所有证明工作——不要委派给子代理。所有循环引擎阶段都在主线程中执行。如果不可用，使用临时文件和进行独立实验。
lean_run_code/tmplake env leanscripts_only (no MCP, no subagents)
scripts_only（无MCP，无子代理）
Use for search and / for validation. Key limitations in this mode:
$LEAN4_SCRIPTSlake env leanlake build- No live goal inspection — is unavailable; you can read the file and check compilation output, but cannot see proof state at a specific line
lean_goal - No tactic testing — is unavailable; edits must be validated by compiling the file (
lean_multi_attempt)lake env lean - No real-time diagnostics — is unavailable; use
lean_diagnostic_messages(from project root) for compilation errors, but feedback is file-level, not line-levellake env lean <file> - Search is script-based — replaces LSP search tools
$LEAN4_SCRIPTS/smart_search.sh
This mode is functional for straightforward proofs but significantly slower and less precise than MCP-backed workflows.
使用进行搜索，使用 / 进行验证。此模式下的关键限制：
$LEAN4_SCRIPTSlake env leanlake build- 无实时目标检查 — 不可用；你可以读取文件并检查编译输出，但无法查看特定行的证明状态
lean_goal - 无策略测试 — 不可用；编辑必须通过编译文件（
lean_multi_attempt）进行验证lake env lean - 无实时诊断 — 不可用；使用
lean_diagnostic_messages（从项目根目录运行）获取编译错误，但反馈是文件级而非行级lake env lean <file> - 搜索基于脚本 — 替代LSP搜索工具
$LEAN4_SCRIPTS/smart_search.sh
此模式适用于简单证明，但比基于MCP的工作流慢得多且精度更低。
review_only (read-only, no edits)
review_only（只读，无编辑）
Read proof state and assess quality. No edits, no commits, no subagent dispatch.
读取证明状态并评估质量。无编辑、无提交、无子代理调度。
File Handling Rules
文件处理规则
Scratch-work ladder (in preference order):
- Live file + MCP tools (,
lean_goal,lean_multi_attempt)lean_diagnostic_messages - for isolated experiments
lean_run_code - scratch files only when
/tmpis unavailable and the experiment must not touch the live filelean_run_code - Never create scratch files in the repo root
File inspection: Use Read and Grep to view source files. Never write Python scripts, temp files, or use pipelines just to read lines from a file you already have access to.
catStaging: Stage only files touched during the current session. Never use or broad glob patterns. Print the exact staged set before committing.
git add -ASee sorry-filling.md for the full scratch-work preference order.
临时工作优先级（按优先顺序）：
- 实时文件 + MCP工具（,
lean_goal,lean_multi_attempt）lean_diagnostic_messages - 用于独立实验
lean_run_code - 仅当不可用且实验不能影响实时文件时，使用
lean_run_code临时文件/tmp - 切勿在仓库根目录创建临时文件
文件检查： 使用Read和Grep查看源文件。切勿编写Python脚本、临时文件或使用管道来读取你已有权限访问的文件内容。
cat暂存： 仅暂存当前会话中修改过的文件。切勿使用或宽泛的通配符模式。提交前打印确切的暂存文件集。
git add -A临时工作的完整优先级请查看sorry-filling.md。
Core Primitives
核心原语
| Script | Purpose | Output |
|---|---|---|
| Find sorries with context | text (default), json, markdown, summary |
| Best-effort axiom scan (top-level declarations) | text |
| Multi-source mathlib search | text |
| Detect optimization patterns | JSON |
| Find declaration usages | text |
Usage: Invoked by commands automatically. See references/ for details.
Invocation contract: Never run bare script names. Always use:
- Python:
${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/script.py" ... - Shell:
bash "$LEAN4_SCRIPTS/script.sh" ... - Report-only calls: add to
--report-only,sorry_analyzer.py,check_axioms_inline.sh— suppresses exit 1 on findings; real errors still exit 1. Do not use in gate commands likeunused_declarations.sh./lean4:checkpoint - Keep stderr visible for Lean scripts (no redirection), so real errors are not hidden.
/dev/null
If is unset or missing, run and stay LSP-only until resolved.
$LEAN4_SCRIPTS/lean4:doctor| 脚本 | 用途 | 输出 |
|---|---|---|
| 查找带上下文的sorry标记 | 文本（默认）、json、markdown、摘要 |
| 尽力而为的公理扫描（顶层声明） | 文本 |
| 多源mathlib搜索 | 文本 |
| 检测优化模式 | JSON |
| 查找声明的使用情况 | 文本 |
使用方式： 由命令自动调用。详情请查看references/。
调用约定： 切勿直接运行脚本名称。请始终使用：
- Python:
${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/script.py" ... - Shell:
bash "$LEAN4_SCRIPTS/script.sh" ... - 仅报告调用：在、
sorry_analyzer.py、check_axioms_inline.sh中添加unused_declarations.sh— 发现问题时不返回退出码1；真正的错误仍会返回退出码1。请勿在--report-only等gate命令中使用。/lean4:checkpoint - 保持Lean脚本的stderr可见（不重定向到），以便不会隐藏真正的错误。
/dev/null
如果未设置或缺失，运行并仅使用LSP工具，直到问题解决。
$LEAN4_SCRIPTS/lean4:doctorAutomation
自动化
/lean4:prove/lean4:autoprove- prove — guided, asks before each cycle. Ideal for interactive sessions.
- autoprove — autonomous, loops with explicit stop budgets. Ideal for unattended runs.
Both share the same cycle engine (plan → work → checkpoint → review → replan → continue/stop) and follow the LSP-first protocol: LSP tools are normative for discovery and search; script fallback only when LSP is unavailable or exhausted. Compiler-guided repair is escalation-only — not the first response to build errors. For complex proofs, they may delegate to internal workflows for deep sorry-filling (with snapshot, rollback, and scope budgets), proof repair, or axiom elimination. You don't invoke these directly.
/lean4:prove/lean4:autoprove- prove — 引导式，每个循环前询问用户。适用于交互式会话。
- autoprove — 自主式，按明确的停止预算循环。适用于无人值守运行。
两者共享相同的循环引擎（规划 → 工作 → 检查点 → 审查 → 重新规划 → 继续/停止），并遵循LSP优先协议：LSP工具是发现和搜索的标准方式；仅当LSP不可用或已用尽时才回退到脚本。编译器引导的修复仅作为升级手段——不是处理构建错误的第一选择。对于复杂证明，它们可能将深度填充sorry标记（带快照、回滚和范围预算）、证明修复或公理消除任务委派给内部工作流。你无需直接调用这些内部工作流。
Skill-Only Behavior
技能专属行为
When editing files without invoking a command, the skill runs one bounded pass:
.lean- Read the goal or error via /
lean_goallean_diagnostic_messages - Search mathlib with up to 2 LSP tools (e.g. +
lean_local_search/lean_leanfinder/lean_leansearch)lean_loogle - Try the Automation Tactics cascade
- Validate with (no project-gate
lean_diagnostic_messagesin this mode)lake build - No looping, no deep escalation, no multi-cycle behavior, no commits
- End with suggestions:
Usefor guided cycle-by-cycle help. Use
/lean4:provefor autonomous cycles with stop safeguards./lean4:autoprove
当编辑文件但未调用命令时，技能会运行一次有限的遍历：
.lean- 通过/
lean_goal读取目标或错误lean_diagnostic_messages - 使用最多2个LSP工具搜索mathlib（例如+
lean_local_search/lean_leanfinder/lean_leansearch）lean_loogle - 尝试自动化策略序列
- 使用验证（此模式下不进行项目级的
lean_diagnostic_messages检查）lake build - 无循环、无深度升级、无多循环行为、无提交
- 最后给出建议：
使用获取循环式引导帮助。 使用
/lean4:prove获取带停止防护的自主循环。/lean4:autoprove
Quality Gate
质量门
A proof is complete when:
- passes
lake build - Zero sorries in agreed scope
- Only standard axioms (,
propext,Classical.choice)Quot.sound - No statement changes without permission
Verification ladder: per-edit → file gate (run from project root) → project gate only. See cycle-engine: Build Target Policy.
lean_diagnostic_messages(file)lake env lean <path/to/File.lean>lake build当满足以下条件时，证明视为完成：
- 通过
lake build - 约定范围内无sorry标记
- 仅使用标准公理（,
propext,Classical.choice）Quot.sound - 未经许可未修改声明
验证流程：每次编辑后运行 → 文件级检查（从项目根目录运行）→ 仅在检查点/最终门时运行项目级检查。详情请查看cycle-engine: Build Target Policy。
lean_diagnostic_messages(file)lake env lean <path/to/File.lean>lake buildCommon Fixes
常见修复
See compilation-errors for error-by-error guidance (type mismatch, unknown identifier, failed to synthesize, timeout, etc.).
错误修复的逐错误指导请查看compilation-errors（类型不匹配、未知标识符、合成失败、超时等）。
Type Class Patterns
类型类模式
lean
-- Local instance for this proof block
haveI : MeasurableSpace Ω := inferInstance
letI : Fintype α := ⟨...⟩
-- Scoped instances (affects current section)
open scoped Topology MeasureTheoryOrder matters: provide outer structures before inner ones.
lean
-- 本证明块的本地实例
haveI : MeasurableSpace Ω := inferInstance
letI : Fintype α := ⟨...⟩
-- 作用域内实例（影响当前section）
open scoped Topology MeasureTheory顺序很重要：先提供外部结构，再提供内部结构。
Automation Tactics
自动化策略
Try in order (stop on first success):
→ → → → → → → → →
rflsimpringlinarithnlinarithomegaexact?apply?grindaesopNote: / query mathlib (slow). and are powerful but may timeout. See grind-tactic for interactive workflows, annotation strategy, and simproc escalation.
exact?apply?grindaesop按顺序尝试（首次成功即停止）：
→ → → → → → → → →
rflsimpringlinarithnlinarithomegaexact?apply?grindaesop注意：/会查询mathlib（速度较慢）。和功能强大但可能超时。交互式工作流、注释策略和simproc升级请查看grind-tactic。
exact?apply?grindaesopTroubleshooting
故障排除
If LSP tools aren't responding, check your operating profile above. In mode, provides search and provides file-level compilation feedback, but live goal inspection, tactic testing, and line-level diagnostics are unavailable. If environment variables (, ) are missing, run to diagnose.
scripts_only$LEAN4_SCRIPTSlake env leanLEAN4_SCRIPTSLEAN4_REFS/lean4:doctorScript environment check:
bash
echo "$LEAN4_SCRIPTS"
ls -l "$LEAN4_SCRIPTS/sorry_analyzer.py"如果LSP工具无响应，请检查上述运行配置文件。在模式下，提供搜索功能，提供文件级编译反馈，但实时目标检查、策略测试和行级诊断不可用。如果环境变量（, ）缺失，运行进行诊断。
scripts_only$LEAN4_SCRIPTSlake env leanLEAN4_SCRIPTSLEAN4_REFS/lean4:doctor脚本环境检查：
bash
echo "$LEAN4_SCRIPTS"
ls -l "$LEAN4_SCRIPTS/sorry_analyzer.py"One-pass discovery for troubleshooting (human-readable default text):
用于故障排除的单次遍历（默认人类可读文本格式）：
${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/sorry_analyzer.py" . --report-only
${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/sorry_analyzer.py" . --report-only
Structured output (optional): --format=json
结构化输出（可选）：--format=json
Counts only (optional): --format=summary
仅统计结果（可选）：--format=summary
**Cold start / fresh worktree:**
- Fresh worktree or after `lake clean`? Prime the cache in that worktree before the first real build.
- Use the project's cache command: `lake cache get` on newer Lake, or `lake exe cache get` where the project still uses the mathlib cache executable.
- If Lean LSP is cold or timing out on first use, run one `lake build` to bootstrap the workspace.
- After bootstrap, return to the normal verification ladder:
`lean_diagnostic_messages(file)` → `lake env lean <path/to/File.lean>` (from project root) → `lake build` only at checkpoint/final gate.
- Do **not** symlink another worktree's `.lake/build`; use Lake cache/artifact mechanisms instead.
**冷启动 / 新工作树：**
- 新工作树或`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缓存/工件机制替代。References
参考资料
Cycle Engine: cycle-engine — shared prove/autoprove logic (stuck, deep mode, falsification, safety)
LSP Tools: lean-lsp-server (quick start), lean-lsp-tools-api (full API — grep for tool names)
^##Search: mathlib-guide (read when searching for existing lemmas), lean-phrasebook (math→Lean translations)
Errors: compilation-errors (read first for any build error), instance-pollution (typeclass conflicts — grep for patterns), compiler-guided-repair (escalation-only repair — not first-pass)
## Sub-Tactics: tactics-reference (tactic lookup — grep ), grind-tactic (SMT-style automation — when simp can't close), simp-reference (simp hygiene + custom simprocs), tactic-patterns, calc-patterns
^### TacticNameProof Development: proof-templates, proof-refactoring (28K — grep by topic), proof-simplification (strategy-level: mathlib search, congr lemmas, helper extraction), sorry-filling
Optimization: proof-golfing (includes safety rules, bounded LSP lemma replacement, bulk rewrites, anti-patterns; escalates to axiom-eliminator), proof-golfing-patterns, performance-optimization (grep by symptom), profiling-workflows (diagnose slow builds/proofs)
Domain: domain-patterns (25K — grep ), measure-theory (28K), axiom-elimination
## AreaStyle: mathlib-style, verso-docs (Verso doc comment roles and fixups)
Custom Syntax: lean4-custom-syntax (read when building notations, macros, elaborators, or DSLs), metaprogramming-patterns (MetaM/TacticM API — composable blocks, elaborators), scaffold-dsl (copy-paste DSL template), json-patterns (json% syntax + ToJson)
Quality: linter-authoring (project-specific linter rules), ffi-interop (FFI, , init, symbol linkage)
@&Workflows: agent-workflows, subagent-workflows, command-examples, learn-pathways (intent taxonomy, game tracks, source handling)
Internals: review-hook-schema, compiler-internals (attributes, specialization, pipeline)
循环引擎： cycle-engine — prove/autoprove共享逻辑（停滞处理、深度模式、证伪、安全）
LSP工具： lean-lsp-server（快速入门）、lean-lsp-tools-api（完整API — 搜索查看工具名称）
^##搜索： mathlib-guide（搜索现有引理时阅读）、lean-phrasebook（数学→Lean翻译）
错误： compilation-errors（遇到任何构建错误时首先阅读）、instance-pollution（类型类冲突 — 搜索查看模式）、compiler-guided-repair（仅作为升级手段的修复 — 非首次尝试）
## Sub-策略： tactics-reference（策略查询 — 搜索）、grind-tactic（SMT风格自动化 — 当simp无法完成时）、simp-reference（simp规范 + 自定义simproc）、tactic-patterns、calc-patterns
^### TacticName证明开发： proof-templates、proof-refactoring（28K — 按主题搜索）、proof-simplification（策略级：mathlib搜索、congr引理、辅助函数提取）、sorry-filling
优化： proof-golfing（包含安全规则、受限LSP引理替换、批量重写、反模式；升级到公理消除器）、proof-golfing-patterns、performance-optimization（按症状搜索）、profiling-workflows（诊断缓慢的构建/证明）
领域： domain-patterns（25K — 搜索）、measure-theory（28K）、axiom-elimination
## Area风格： mathlib-style、verso-docs（Verso文档注释角色与修正）
自定义语法： lean4-custom-syntax（构建符号、宏、解析器或DSL时阅读）、metaprogramming-patterns（MetaM/TacticM API — 可组合块、解析器）、scaffold-dsl（可复制粘贴的DSL模板）、json-patterns（json%语法 + ToJson）
质量： linter-authoring（项目特定检查规则）、ffi-interop（FFI、、初始化、符号链接）
@&工作流： agent-workflows、subagent-workflows、command-examples、learn-pathways（意图分类、学习路径、源处理）
内部实现： review-hook-schema、compiler-internals（属性、特化、流水线）