Name: lean4
Author: cameronfreer

Use when editing .lean files, debugging Lean 4 builds (type mismatch, sorry, failed to synthesize instance, axiom warnings, lake build errors), searching mathlib for lemmas, formalizing mathematics in Lean, finding a counterexample to, refuting, or disproving a Lean statement, or learning Lean 4 con

Lean 4 Theorem Proving 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. 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](references/mathlib style.md) for breaking strategies when lines exceed 100. Mathlib style quick check. For ordinary mathematical lambdas, write fun x ↦ ... ( \mapsto ), not fun x = ... . Use = for match / do branches and metaprogramming callback idioms. Prefer show P by tac for tactic proofs; use show P from term only for term proofs. See [mathlib style](references/mathlib style.md). Preserve statements and signatures — they're the file's contract. Theorem/lemma statements and type signatures are off limits unless the user explicitly requests changes; changing them can break callers or alter the theorem being proved. If a proof seems to require changing a statement or adding a custom axiom, stop and discuss first because that changes the contract or the proof's trust basis. Exception: within synthesis wrappers ( /lean4:formalize , /lean4:autoformalize ), session generated declarations may be redrafted under the outer loop statement safety rules; see cycle engine.md. Docstrings are scoped by workflow. Existing docstrings are API. The default is Rule A — any workflow that mutates existing declarations follows it unless the user explicitly requests docstring changes: Mode May do Boundary A — editing existing declarations (e.g. /lean4:prove , sorry filler deep , golf, refactor, any agent editing existing decls) adjust inline comments in proof bodies never rewrite an existing docstring — explicit user request only B — review ( /lean4:review ) flag weak/missing docstrings and propose replacement text in the report read only — never mutates files C — new file / new decl generation ( /lean4:draft , /lean4:formalize , /lean4:autoformalize ) emit module/declaration docstrings on files or declarations it newly creates existing docstrings stay under Rule A Per command policy lives in each command's doc. The docstring split applies in every project; when the mathlib Template Gate selects the mathlib header, Rule C fills its module docstring slot — Rule C neither selects nor redefines the [template](references/mathlib style.md 1 file header copyright module imports critical). Commands Command Purpose /lean4:draft Draft Lean declaration skeletons from informal claims /lean4:formalize Interactive formalization — drafting plus guided proving /lean4:autoformalize Autonomous end to end formalization from informal sources /lean4:prove Guided cycle by cycle theorem proving with explicit checkpoints /lean4:autoprove Autonomous multi cycle theorem proving with explicit stop budgets /lean4:disprove Guided counterexample search with certified refutation /lean4:checkpoint Save progress with a safe commit checkpoint /lean4:review Read only code review of Lean proofs /lean4:refactor Leverage mathlib, extract helpers, simplify proof strategies /lean4:golf Improve Lean proofs for directness, clarity, performance, and brevity /lean4:learn Interactive teaching and mathlib exploration /lean4:diagnose Diagnostics, cleanup, and migration help /lean4: names are the native plugin's command aliases and also serve as stable workflow names throughout this documentation. On hosts without command registration (skill only or portable installs), invoke the lean4 skill with your host's normal syntax and ask for the named workflow — e.g., "Use the guided prove workflow on Foo.lean:42 ." This plugin ships a host agnostic parser ( lib/command args/ ) that covers the parser decidable startup rules of the seven parameter heavy commands ( draft , learn , formalize , autoformalize , prove , autoprove , disprove ). 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 ( checkpoint , review , refactor , golf , diagnose ) remain model parsed. When a host adapter installs the UserPromptSubmit hook, the parser runs before the model sees a /lean4: prompt matching one of the seven covered commands, injects a validated invocation 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](references/command invocation.md) contract. Commands always announce resolved inputs, reject invalid startup configs before doing work, and treat wall clock budgets like max total runtime as best effort. Which Command? Situation Command Draft a Lean skeleton (skeleton by default) /lean4:draft Draft + prove interactively /lean4:formalize Filling sorries (interactive) /lean4:prove Filling sorries (unattended) /lean4:autoprove Searching for a counterexample to refute a claim /lean4:disprove Save point (per file + project build, best effort axiom scan, commit) /lean4:checkpoint Quality check (read only) /lean4:review Simplify proof strategies (mathlib leverage, helpers) /lean4:refactor Optimizing compiled proofs /lean4:golf New to this project / exploring /lean4:learn mode=repo Navigating mathlib for a topic /lean4:learn mode=mathlib Something not working /lean4:diagnose Formalize + prove end to end (unattended) /lean4:autoformalize source=... claim select=first out=... Contributing (lean4 contribute plugin) If the lean4 contribute plugin is installed, you may suggest these commands at natural stopping points. Rules: 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?" → /lean4 contribute: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?" → /lean4 contribute: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?" → /lean4 contribute:share 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 lean4 contribute plugin and I can draft that report for you here." See the [lean4 contribute README](https://github.com/cameronfreer/lean4 skills/blob/main/plugins/lean4 contribute/README.md installation) for setup. Typical Workflow Use /lean4:learn at any point to explore repo structure or navigate mathlib. Three entry points: /lean4:draft for skeletons, /lean4:formalize for interactive synthesis (draft + guided proving), /lean4:autoformalize for unattended source to proof. Refutation branch: Use /lean4:disprove <target when the goal is to refute a statement rather than prove it. Always interactive; runs a 6 phase cycle (Plan → Work → Checkpoint → Review → Accumulate → Continue/Stop) where Phase 1 generates dynamic Step 0 / Step 1 / Step 2 menus seeded by accumulated evidence (Phase 5 — Accumulate — replaces prove's Replan). Each cycle is a widening search pass over the same target. Append only — it adds a T counterexample theorem alongside the original sorry, never rewrites the original declaration. Requires Python 3.11+ (registry loader). See [disprove engine.md](references/disprove engine.md), incl. its [Implementation Status](references/disprove engine.md implementation status) table (deterministic vs model mediated vs deferred). Notes: /lean4:prove asks before each cycle; /lean4:autoprove loops autonomously with explicit stop budgets Both trigger /lean4:review at configured intervals ( review every ) When reviews run (via review every ), they act as gates: review → replan → continue. In prove, replan requires user approval; in autoprove, replan auto continues Review supports mode=batch (default) or mode=stuck (triage); review is always read only /lean4:autoformalize wraps draft+autoprove in a single command (source → claims → skeletons → proofs); replaces autoprove formalize=auto Proof engines ( prove / autoprove ) never modify declaration headers (header fence) /lean4:disprove reports REFUTED only when Lean typechecks the negation; otherwise WITNESS UNCERTIFIED or INCONCLUSIVE If you hit environment issues, run /lean4:diagnose to diagnose LSP Tools (Preferred) Sub second feedback and search tools (LeanSearch, Loogle, LeanFinder) via Lean LSP MCP: lean run code is for isolated scratch experiments, not a substitute for live proof state inspection via lean goal / lean multi attempt / lean diagnostic messages . Prefer live file tools when the question depends on actual file context. Capabilities Capability Required Check Fallback Lean / Lake yes lean version , lake version none — run /lean4:diagnose Python 3 yes (scripts) python3 version or persistent $LEAN4 PYTHON BIN none for script dependent operations Helper runtime path yes (scripts) trusted Codex bin dir / scripts dir , or persistent $LEAN4 SCRIPTS use the diagnose workflow; stay LSP only if unresolved Lean LSP MCP no try lean goal on any .lean file scripts + lake env lean (file level only) lean run code no try calling it lake env lean on temp file lean code actions 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 Operating Profiles The skill adapts to what's available. Determine your profile by checking capabilities above, then follow the corresponding guidance. Runtime path resolution Resolve the helper runtime in this order: 1. Trusted native Codex plugin: SessionStart context contains lean4 plugin runtime=