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.

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.

Commands

Command

Purpose

/lean4:formalize

Turn informal math into Lean statements

/lean4:prove

Guided cycle-by-cycle theorem proving

/lean4:autoprove

Autonomous multi-cycle proving with stop rules

/lean4:checkpoint

Verified save point (build + axiom check + commit)

/lean4:review

Quality audit (

--mode=batch

or

--mode=stuck

)

/lean4:golf

Optimize proofs for brevity

/lean4:learn

Interactive teaching and mathlib exploration

/lean4:doctor

Plugin troubleshooting and migration help

Which Command?

Situation

Command

Draft a Lean statement from an informal claim

/lean4:formalize

Filling sorries (interactive)

/lean4:prove

Filling sorries (unattended)

/lean4:autoprove

Verified save point

/lean4:checkpoint

Quality check (read-only)

/lean4:review

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:doctor

Typical Workflow

/lean4:prove Guided cycle-by-cycle proving (asks before each cycle)

/lean4:autoprove Autonomous multi-cycle proving (runs with stop rules)

↓

/lean4:golf Optimize proofs (optional, prompted at end)

↓

/lean4:checkpoint Create verified save point

Use

/lean4:learn

at any point to explore repo structure or navigate mathlib. Use

/lean4:formalize

to turn informal math into Lean statements.

Notes:

/lean4:prove

asks before each cycle;

/lean4:autoprove

loops autonomously with hard stop conditions

Both trigger

/lean4:review

at configured intervals (

--review-every

)

When reviews run (via

--review-every

), they act as gates: review → replan → approval → continue

Review supports

--mode=batch

(default) or

--mode=stuck

(triage)

If you hit environment issues, run

/lean4:doctor

to diagnose

LSP Tools (Preferred)

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

Core Primitives

Script

Purpose

Output

sorry_analyzer.py

Find sorries with context

text (default), json, markdown, summary

check_axioms_inline.sh

Check for non-standard axioms

text

smart_search.sh

Multi-source mathlib search

text

find_golfable.py

Detect optimization patterns

JSON

find_usages.sh

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

--report-only

to

sorry_analyzer.py

,

check_axioms_inline.sh

,

unused_declarations.sh

— suppresses exit 1 on findings; real errors still exit 1. Do not use in gate commands like

/lean4:checkpoint

.

Keep stderr visible for Lean scripts (no

/dev/null

redirection), so real errors are not hidden.

If

$LEAN4_SCRIPTS

is unset or missing, run

/lean4:doctor

and stay LSP-only until resolved.

Automation

/lean4:prove

and

/lean4:autoprove

handle most tasks:

prove

— guided, asks before each cycle. Ideal for interactive sessions.

autoprove

— autonomous, loops with hard stop rules. 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. Skill-Only Behavior When editing .lean files without invoking a command, the skill runs one bounded pass : Read the goal or error via lean_goal / lean_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 lean_diagnostic_messages (no project-gate lake build in this mode) No looping, no deep escalation, no multi-cycle behavior, no commits End with suggestions: Use /lean4:prove for guided cycle-by-cycle help. Use /lean4:autoprove for autonomous cycles with stop safeguards. Quality Gate A proof is complete when: lake build passes Zero sorries in agreed scope Only standard axioms ( propext , Classical.choice , Quot.sound ) No statement changes without permission Verification ladder: lean_diagnostic_messages(file) per-edit → lake env lean file gate (run from project root) → lake build project gate only. See cycle-engine: Build Target Policy . Common Fixes See compilation-errors for error-by-error guidance (type mismatch, unknown identifier, failed to synthesize, timeout, etc.). Type Class Patterns -- Local instance for this proof block haveI : MeasurableSpace Ω := inferInstance letI : Fintype α := ⟨...⟩ -- Scoped instances (affects current section) open scoped Topology MeasureTheory Order matters: provide outer structures before inner ones. Automation Tactics Try in order (stop on first success): rfl → simp → ring → linarith → nlinarith → omega → exact? → apply? → grind → aesop Note: exact? / apply? query mathlib (slow). grind and aesop are powerful but may timeout. Troubleshooting If LSP tools aren't responding, scripts provide fallback for all operations. If environment variables ( LEAN4_SCRIPTS , LEAN4_REFS ) are missing, run /lean4:doctor to diagnose. Script environment check: 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

Structured output (optional): --format=json

Counts only (optional): --format=summary

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

Sub-

for patterns), compiler-guided-repair (escalation-only repair — not first-pass) Tactics: tactics-reference (tactic lookup — grep ^### TacticName ), grind-tactic (SMT-style automation — when simp can't close), simp-reference (simp hygiene + custom simprocs), tactic-patterns , calc-patterns Proof Development: proof-templates , proof-refactoring (28K — grep by topic), 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

Area

), measure-theory (28K), axiom-elimination Style: 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) Quality: linter-authoring (project-specific linter rules), ffi-patterns (C/ObjC bindings via Lake) Workflows: agent-workflows , subagent-workflows , command-examples , learn-pathways (intent taxonomy, game tracks, source handling) Internals: review-hook-schema