Lean4

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 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 (/lean4:formalize, /lean4:autoformalize), session-generated declarations may be redrafted under the outer-loop statement-safety rules; see cycle-engine.md.

Commands

This plugin ships a host-agnostic parser (lib/command_args/) that covers the parser-decidable startup rules of the six parameter-heavy commands (draft, learn, formalize, autoformalize, prove, autoprove). 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, doctor) 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 six 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 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?

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.

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 for setup.

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 /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.

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)
• 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
lean_diagnostic_messages(file)                  # Per-file error/warning check
lean_code_actions(file, line)                   # Resolve "Try this" suggestions to edits

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

Operating Profiles

The skill adapts to what's available. Determine your profile by checking capabilities above, then follow the corresponding guidance.

full (all capabilities)

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 lean_run_code is unavailable, use /tmp scratch files with lake env lean for isolated experiments.

mcp_main_only (MCP available, no subagent dispatch)

MCP works in the main thread. Run all proof work directly — do not delegate to subagents. All cycle-engine phases execute in-thread. If lean_run_code is unavailable, use /tmp scratch files with lake env lean for isolated experiments.

scripts_only (no MCP, no subagents)

Use $LEAN4_SCRIPTS for search and lake env lean / lake build for validation. Key limitations in this mode:

• No live goal inspection — lean_goal is unavailable; you can read the file and check compilation output, but cannot see proof state at a specific line
• No tactic testing — lean_multi_attempt is unavailable; edits must be validated by compiling the file (lake env lean)
• No real-time diagnostics — lean_diagnostic_messages is unavailable; use lake env lean <file> (from project root) for compilation errors, but feedback is file-level, not line-level
• Search is script-based — $LEAN4_SCRIPTS/smart_search.sh replaces LSP search tools

This mode is functional for straightforward proofs but significantly slower and less precise than MCP-backed workflows.

review_only (read-only, no edits)

Read proof state and assess quality. No edits, no commits, no subagent dispatch.

File Handling Rules

Scratch-work ladder (in preference order): 1. Live file + MCP tools (lean_goal, lean_multi_attempt, lean_diagnostic_messages) 2. lean_run_code for isolated experiments 3. /tmp scratch files only when lean_run_code is unavailable and the experiment must not touch the live file 4. 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 cat pipelines just to read lines from a file you already have access to.

Staging: Stage only files touched during the current session. Never use git add -A or broad glob patterns. Print the exact staged set before committing.

See sorry-filling.md for the full scratch-work preference order.

Core Primitives

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 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.

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 <path/to/File.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. See grind-tactic for interactive workflows, annotation strategy, and simproc escalation.

Troubleshooting

If LSP tools aren't responding, check your operating profile above. In scripts_only mode, $LEAN4_SCRIPTS provides search and lake env lean provides file-level compilation feedback, but live goal inspection, tactic testing, and line-level diagnostics are unavailable. 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

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.

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), 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 ## 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), 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)

Agent Workflow Examples

Internal reference: These workflows are orchestrated by commands. You typically don't invoke them directly.

For Claude Code users: See subagent-workflows.md for user-facing delegation patterns.

Review source is chosen at prove/autoprove start. External review provides advice only—it cannot apply fixes directly.

Extended workflow examples for Lean4 plugin internal workflows.

---

sorry-filler-deep

Helper Extraction Example

## Sorry Filling Plan

**Target:** Core.lean:156 - `filter_convergence`

**Why it's hard:**
- Need Filter.Eventually lemma but it doesn't exist yet
- Type class instance ordering issue
- Existing proof approach requires an intermediate bridging lemma

**Strategy:**
1. Extract helper lemma `filter_eventually_of_set` bridging Set and Filter
2. Add import for `Mathlib.Order.Filter.Basic`
3. Prove main theorem using helper
4. Verify dependent theorems still work

**Estimated difficulty:** medium
**Estimated phases:** 3

---

## Phase 1 Complete

**Actions taken:**
- Added `filter_eventually_of_set` helper lemma
- Added import for `Mathlib.Order.Filter.Basic`

**Compile status:** ✓ Success

**Next phase:** Fill original sorry using helper

---

## Phase 2 Complete

**Actions taken:**
- Filled sorry using helper lemma
- Proof: 4 lines using `filter_eventually_of_set` + `Filter.Eventually.mono`

**Compile status:** ✓ Success

---

## Sorry Filled Successfully

**Target:** Core.lean:156
**Strategy used:** helper extraction
**Phases completed:** 2
**Total edits:** 2 files changed

**Summary:**
- Sorry eliminated: ✓
- Proof type: helper-lemmas
- Complexity: 4 lines of proof
- New helpers introduced: 1 (`filter_eventually_of_set`)
- Axioms introduced: 0

**Verification:**
- File compiles: ✓
- Dependent theorems work: ✓
- No unexpected axioms: ✓

---

proof-repair

Type Mismatch Repair

{
  "errorHash": "type_mismatch_a3f2",
  "errorType": "type_mismatch",
  "message": "type mismatch\n  h1\nhas type\n  Measurable f\nbut is expected to have type\n  Continuous f",
  "file": "Core.lean",
  "line": 42,
  "goal": "⊢ Continuous f",
  "localContext": ["h1 : Measurable f", "h2 : Integrable f μ"]
}

Stage 1 output:

--- Core.lean
+++ Core.lean
@@ -42,1 +42,1 @@
-  exact h1
+  exact Continuous.of_discrete h1

Build fails, error persists. Stage 1 retry:

--- Core.lean
+++ Core.lean
@@ -42,1 +42,2 @@
-  exact h1
+  haveI : DiscreteTopology α := inferInstance
+  exact continuous_of_discreteTopology

Build succeeds. ✓

Instance Synthesis Repair

{
  "errorType": "synth_instance",
  "message": "failed to synthesize instance\n  MeasurableSpace β",
  "file": "Core.lean",
  "line": 89
}

Stage 1 outputs (after 3 failures, escalates to Stage 2):

--- Core.lean
+++ Core.lean
@@ -87,0 +87,1 @@
+variable [MeasurableSpace β] in

Unknown Identifier Repair

{
  "errorType": "unknown_ident",
  "message": "unknown identifier 'continuous_real'",
  "file": "Core.lean",
  "line": 15
}

LSP search: lean_leanfinder("continuous real function") → Real.continuous_ofReal Fallback if needed: $LEAN4_SCRIPTS/search_mathlib.sh "continuous.*real" name

--- Core.lean
+++ Core.lean
@@ -1,0 +1,1 @@
+import Mathlib.Topology.Instances.Real
@@ -15,1 +16,1 @@
-  exact continuous_real
+  exact Real.continuous_ofReal

---

proof-golfer

Verified Inlining Example

File: Core.lean
Finding patterns...

Pattern found at line 45:
  let x := complex_expr
  have h := property x
  exact h

Running: $LEAN4_SCRIPTS/analyze_let_usage.py Core.lean --line 45
Result: x used 1 time, h used 1 time

Safety: ✓ Safe to inline (both used ≤2 times)

Before (3 lines):
  let x := complex_expr
  have h := property x
  exact h

After (1 line):
  exact property complex_expr

Building... ✓

Savings: 2 lines, ~30 tokens

False Positive Detection

Pattern found at line 78:
  let bound := expensive_computation
  ...uses bound 6 times...

Running: $LEAN4_SCRIPTS/analyze_let_usage.py Core.lean --line 78
Result: bound used 6 times

Safety: ✗ SKIP - would expand code 6× (from 1 expr to 6)

Skipping this optimization.

Saturation Report

Proof Golfing Results:

File: Core.lean
Patterns attempted: 15
Successful: 8
Failed/Reverted: 2
Skipped (safety): 5

Total savings:
- Lines: 145 → 127 (12% reduction)
- Tokens: estimated 2100 → 1850 tokens

Saturation indicators:
- Success rate: 8/15 = 53%
- Last 3 attempts: 1 success, 2 skips

Status: Good progress, some room remains.
Continue? (yes/no)

LSP Lemma Replacement

Pattern found at line 30:
  exact custom_continuous_comp f g

LSP search: lean_local_search("continuous comp") → Continuous.comp
Replacement: lean_multi_attempt(file, 30, ["exact Continuous.comp f g"])
  Result: ✓ passes

Before (1 line):
  exact custom_continuous_comp f g

After (1 line + import):
  exact Continuous.comp f g

Diagnostics: lean_diagnostic_messages(file) → no errors
Import added: Mathlib.Topology.Basic

Savings: replaced custom helper with mathlib lemma
Handoff: not needed (single-line, no statement change)

---

axiom-eliminator

Migration Plan Example

## Axiom Elimination Plan

**Total custom axioms:** 4
**Target:** 0 custom axioms

### Axiom Inventory

1. **helper_continuous** (Core.lean:23)
   - Type: mathlib_search
   - Used by: 3 theorems
   - Strategy: Search mathlib for equivalent
   - Priority: high

2. **measure_finite** (Measure.lean:45)
   - Type: compositional
   - Used by: 5 theorems
   - Strategy: Compose from mathlib lemmas
   - Priority: high

3. **set_countable** (Core.lean:89)
   - Type: structural_refactor
   - Used by: 2 theorems
   - Strategy: Refactor to use Countable typeclass
   - Priority: medium

4. **magic_bound** (Bounds.lean:12)
   - Type: needs_deep_expertise
   - Used by: 1 theorem
   - Strategy: Convert to sorry for later filling
   - Priority: low

### Elimination Order

**Phase 1: Low-hanging fruit**
- helper_continuous (mathlib_search)
- measure_finite (compositional)

**Phase 2: Medium difficulty**
- set_countable (structural_refactor)

**Phase 3: Hard cases**
- magic_bound (convert to sorry)

Per-Axiom Progress Report

## Axiom Eliminated: helper_continuous

**Location:** Core.lean:23
**Strategy:** mathlib_import

**Search results:**
LSP: lean_leanfinder("continuous composition") → Continuous.comp (Mathlib.Topology.Basic)
Fallback: $LEAN4_SCRIPTS/search_mathlib.sh "continuous.*comp" name

**Changes made:**
- Removed `axiom helper_continuous`
- Added `import Mathlib.Topology.Basic`
- Replaced with `theorem helper_continuous := Continuous.comp`

**Verification:**
- Compile: ✓
- Axiom count: 4 → 3 ✓
- Dependents work: ✓

**Next target:** measure_finite

Final Summary

## Axiom Elimination Complete

**Starting axioms:** 4
**Ending axioms:** 0
**Eliminated:** 4

**By strategy:**
- Mathlib import: 2
- Compositional proof: 1
- Structural refactor: 1
- Converted to sorry: 0

**Files changed:** 3
**Helper lemmas added:** 2

**Quality checks:**
- All files compile: ✓
- No new axioms introduced: ✓
- Dependent theorems work: ✓
- Sorry count unchanged: ✓

Axiom Elimination Reference

Quick reference for systematically eliminating custom axioms from Lean 4 proofs.

Standard vs Custom Axioms

Standard mathlib axioms (ACCEPTABLE):

• Classical.choice (axiom of choice)
• propext (propositional extensionality)
• quot.sound / Quot.sound (quotient soundness)

Custom axioms (MUST ELIMINATE):

• Any axiom declarations in your code
• Dependencies on unproven theorems

Verification

Check axiom usage:

bash $LEAN4_SCRIPTS/check_axioms_inline.sh FILE.lean
bash $LEAN4_SCRIPTS/check_axioms_inline.sh .          # scan entire project

For individual theorems:

lake env lean --run <<EOF
#print axioms theoremName
EOF

Using the Axiom Check Script

Always prefer the script over manual checks:

$LEAN4_SCRIPTS/check_axioms_inline.sh path/to/file.lean
$LEAN4_SCRIPTS/check_axioms_inline.sh src/   # scan directory recursively

The script handles namespace inference and filters standard axioms automatically.

Why use the script:

• Automatically detects the namespace from the file
• Filters out standard mathlib axioms (propext, quot.sound, Classical.choice)
• Provides clear reporting of non-standard axiom usage
• Handles cleanup of temporary modifications

Limitations:

• Private/protected/local declarations cannot be checked (they're not exported)
• Only detects the first namespace and top-level declarations at column 0
• Nested namespaces may be missed
• Declarations with access modifiers will show warnings (not errors)

If you must check manually:

namespace MyNamespace
#print axioms myDeclaration
end MyNamespace

Note: Private declarations will still fail with unknownIdentifier - this is expected.

DO NOT create manual axiom-checking files like `/tmp/check_axioms.lean`:

• The script is more reliable and handles edge cases
• Manual files often miss namespace context
• Manual files need cleanup afterward

Elimination Workflow

Phase 1: Audit Current State

1. Run axiom checker on all files 2. List all custom axioms with locations 3. Identify dependencies (which theorems use which axioms) 4. Prioritize by impact (eliminate high-usage axioms first)

Phase 2: Document Elimination Plan

For each axiom, document:

axiom helper_theorem : P
-- TODO: Eliminate axiom
-- Strategy: [search pattern OR proof technique]
-- Required lemmas: [mathlib lemmas needed]
-- Difficulty: [easy/medium/hard]
-- Priority: [high/medium/low - based on usage count]
-- Est. time: [time estimate]

Phase 3: Search Mathlib Exhaustively

60% of axioms already exist as theorems in mathlib!

Search by name:

bash $LEAN4_SCRIPTS/search_mathlib.sh "axiom_name_pattern" name

Search by type/description:

bash $LEAN4_SCRIPTS/smart_search.sh "property description" --source=leansearch

Search by type pattern:

bash $LEAN4_SCRIPTS/smart_search.sh "type signature pattern" --source=loogle

Phase 4: Eliminate Axioms

Five common patterns:

Pattern 1: "It's in mathlib" (60%)

• Search finds existing theorem
• Replace axiom with theorem and import
• Replace body with := mathlib_lemma

Pattern 2: "Compositional proof" (30%)

• Combine 2-3 existing mathlib lemmas
• Prove using standard tactics
• Replace axiom with actual proof

Pattern 3: "Needs domain expertise" (9%)

• Break into smaller lemmas
• Prove components using mathlib
• Combine for final result

Pattern 4: "Actually false" (1%)

• Original axiom too strong
• Weaken to provable version
• Update dependent theorems

Pattern 5: "Placeholder for sorry" (common during development)

• Convert axiom to theorem with sorry
• Fill using sorry-filling workflow
• See sorry-filling.md

Elimination Strategies by Type

Simple Lemmas

-- Before
axiom simple_fact : A → B

-- After (search mathlib)
import Mathlib.Data.Foo
theorem simple_fact : A → B := mathlib_existing_lemma

Compositional Proofs

-- Before
axiom complex_fact : Big_Statement

-- After (prove from components)
theorem complex_fact : Big_Statement := by
  have h1 := mathlib_lemma_1
  have h2 := mathlib_lemma_2
  exact combine h1 h2

Structural Refactors

-- Before
axiom infrastructure : Property

-- After (add structure)
-- 1. Introduce helper lemmas
private lemma helper1 : SubProperty := by ...
private lemma helper2 : AnotherSubProperty := by ...

-- 2. Combine for main result
theorem infrastructure : Property := by
  apply helper1
  exact helper2

Handling Dependencies

If axiom A depends on axiom B: 1. Eliminate B first (bottom-up approach) 2. Document dependency chain 3. Verify elimination doesn't break A 4. Then eliminate A

Dependency tracking:

# Find what uses an axiom
bash $LEAN4_SCRIPTS/find_usages.sh axiom_name

Progress Tracking

After each elimination:

# Verify axiom count decreased
bash $LEAN4_SCRIPTS/check_axioms_inline.sh FILE.lean

# Compare before/after
echo "Before: N custom axioms"
echo "After: M custom axioms"
echo "Eliminated: $((N - M))"

Expected elimination rate:

• Easy axioms: 2-3 per hour
• Medium axioms: 1-2 per day
• Hard axioms: 2-5 days each

Migration Plan Template

For large axiom elimination work:

## Axiom Elimination Plan

Total custom axioms: N
Target: 0 custom axioms

### Phase 1: Low-hanging fruit (Est: X days)
- [ ] axiom_1 (type: mathlib_search)
- [ ] axiom_2 (type: simple_composition)
- [ ] axiom_3 (type: mathlib_search)

### Phase 2: Medium difficulty (Est: Y days)
- [ ] axiom_4 (type: structural_refactor)
- [ ] axiom_5 (type: domain_expertise)

### Phase 3: Hard cases (Est: Z days)
- [ ] axiom_6 (type: needs_deep_refactor)

Estimated total: X+Y+Z days

Common Pitfalls

❌ Don't:

• Add new axioms while eliminating old ones
• Skip mathlib search (60% hit rate!)
• Eliminate without testing dependents
• Give up after first search failure
• Use stronger axiom to replace weaker one

✅ Do:

• Search thoroughly (multiple strategies)
• Test with lake build after each elimination
• Track progress (axiom count trending down)
• Document hard cases for future work
• Prove shims for backward compatibility

When to Keep Axioms

Rare acceptable cases (WITH user approval): 1. Foundational axioms for new domain (e.g., new mathematical structure) 2. Interface with external systems (FFI, oracles) 3. Temporary scaffolding with CLEAR timeline

Requires:

• Explicit user approval
• Documented elimination plan
• Timeline for removal
• Not acceptable for mathlib contributions

Integration with Subagents

axiom-eliminator agent can:

• Search mathlib exhaustively for each axiom
• Try multiple proof strategies
• Generate elimination patches
• Track progress across batch

Use for:

• Projects with 10+ axioms
• Systematic cleanup work
• When you need to focus on other tasks

Keep human for:

• Novel mathematical insights
• Design decisions
• Hard cases needing creativity

Output Expectations

Agent output expectations:

• Outline plan FIRST (bullet points)
• Show search results
• Propose elimination strategy
• Apply in small batches
• Report progress after each batch
• Total output: ~2000-3000 tokens per axiom

Calc Chain Patterns

Overview

Calc chains are powerful for chaining equalities and inequalities, but they interact with simplification in non-obvious ways. This guide shows common patterns and pitfalls.

Quick Reference

Key principles: 1. After simp, check the actual goal state FIRST - simp may or may not simplify depending on context 2. Start calc from whatever the goal actually is - not what you expect it to be 3. Context matters - filter_upwards with ω enables more simp simplifications than without 4. Use canonical forms - (m:ℝ)⁻¹ not 1/(m:ℝ) (but only if simp produced it) 5. Don't fight simp - work with its transformations, not against them 6. One simplification pass - let simp do all transformations, then reason

Debugging checklist when calc fails:

• [ ] Did I use simp before calc?
• [ ] Did I check the actual goal state after simp? (Use LSP or sorry)
• [ ] Am I starting calc from the ACTUAL goal, not the expected simplified form?
• [ ] If simp didn't simplify, am I converting in the first calc step?
• [ ] Am I using canonical notation consistently?

Critical Pattern: simp Before calc

The Problem: After simp [Real.norm_eq_abs] (or any simp), you must start the calc chain with whatever form the goal is actually in after simp runs. This might be the simplified form OR the original form, depending on context.

What `simp [Real.norm_eq_abs]` CAN do (context-dependent): 1. Converts ‖x‖ to |x| (Real.norm_eq_abs) 2. Converts |a * b| to |a| * |b| (abs_mul) 3. Simplifies |positive| to positive (abs_of_pos when provable) 4. Converts 1/(m:ℝ) to (m:ℝ)⁻¹ (one_div) - only in some contexts

Example 1: When simp DOES simplify (with ω context)

-- ❌ WRONG: calc chain starts with original expression
filter_upwards with ω; simp [Real.norm_eq_abs]
calc |(1/(m:ℝ)) * ∑ k : Fin m, f k|
    = |(m:ℝ)⁻¹ * ∑ k : Fin m, f k| := by rw [one_div]
  _ = (m:ℝ)⁻¹ * |∑ k : Fin m, f k| := by rw [abs_mul, abs_of_pos]; positivity
  _ ≤ ...

Error: invalid 'calc' step, left-hand side is (m:ℝ)⁻¹ * |∑ ...| but is expected to be |(1/(m:ℝ)) * ∑ ...|

Why: The filter_upwards with ω; simp [Real.norm_eq_abs] already transformed the goal from |(1/(m:ℝ)) * ∑...| to (m:ℝ)⁻¹ * |∑...|

-- ✅ CORRECT: calc chain starts with already-simplified form
filter_upwards with ω; simp [Real.norm_eq_abs]
-- Note: simp already converted |(1/m) * ∑...| to (m:ℝ)⁻¹ * |∑...|
calc (m:ℝ)⁻¹ * |∑ k : Fin m, f k|
    _ ≤ (m:ℝ)⁻¹ * ∑ k : Fin m, |f k| := by
      gcongr; exact Finset.abs_sum_le_sum_abs _ _
  _ ≤ ...

Success: Start with the simplified form directly, no redundant steps.

Example 2: When simp does NOT simplify (no ω context)

-- Context: No filter_upwards, different simp lemmas
-- Goal: ‖1 / (m:ℝ) * ∑ i : Fin m, ...‖ ≤ bound

-- ✅ CORRECT: calc starts with ORIGINAL form (simp didn't simplify it)
simp only [Real.norm_eq_abs, zero_add]
calc |1 / (m:ℝ) * ∑ i : Fin m, ...|
    = (m:ℝ)⁻¹ * |∑ i : Fin m, ...| := by
      rw [one_div, abs_mul, abs_of_pos]; positivity
  _ ≤ ...

Why this works: Without the filter_upwards with ω context, simp [Real.norm_eq_abs] did NOT convert |1/(m:ℝ) * ∑...| to (m:ℝ)⁻¹ * |∑...|, so the calc must start with the original form and perform the conversion explicitly in the first step.

Key difference:

• With `filter_upwards with ω`: simp simplifies → start calc with simplified form
• Without that context: simp doesn't simplify → start calc with original form

Performance Impact

Removing redundant calc steps:

• Saves lines: 15+ redundant steps eliminated across typical session
• Reduces elaboration time: From timeout to instant in complex proofs
• Clearer proofs: Readers see the actual reasoning, not simp artifacts

Critical Nuance: When simp DOES vs DOES NOT Simplify

Important discovery: simp [Real.norm_eq_abs] behavior depends on context.

With filter_upwards with ω context, simp DOES convert |1/(m:ℝ) * ∑...| to (m:ℝ)⁻¹ * |∑...|:

-- ✅ simp DOES simplify (with ω context)
filter_upwards with ω; simp [Real.norm_eq_abs]
calc (m:ℝ)⁻¹ * |∑...|  -- Start with simplified form
    _ ≤ ...

Without that context, simp DOES NOT perform the conversion:

-- ✅ simp does NOT simplify (no ω context)
simp only [Real.norm_eq_abs, zero_add]
calc |1 / (m:ℝ) * ∑...|  -- Start with ORIGINAL form
    = (m:ℝ)⁻¹ * |∑...|   -- First step: do conversion explicitly
  _ ≤ ...

General rule: After simp, always check the goal state to see what form it's in. Start calc from whatever the goal actually is, not what you expect it to be.

Debugging Workflow

If you get "invalid 'calc' step" errors:

1. Check what simp did: Add trace_simp to see transformations

   filter_upwards with ω
   trace_simp [Real.norm_eq_abs]  -- Shows what simp simplified
   calc ...

2. Inspect goal state: Use LSP or sorry to see current goal

   filter_upwards with ω; simp [Real.norm_eq_abs]
   sorry  -- Check goal state here

3. Start calc from actual goal: Match what you see in goal state, not what you expect

• If goal is (m:ℝ)⁻¹ * |∑...|, start calc there
• If goal is |1/(m:ℝ) * ∑...|, start calc there and convert in first step

When This Pattern Applies

This pattern applies whenever:

• Using simp before calc (not just Real.norm_eq_abs)
• Simp lemmas that transform the goal structure (division, abs, norms)
• Building calc chains in measure theory (norms and integrability often simplified)

General rule: After any simp, check the goal state before starting calc.

Type Annotations in Calc Chains

Use canonical forms that simp produces:

-- ❌ WRONG: Non-canonical form
calc |(1/(m:ℝ)) * ∑...|  -- simp will convert to (m:ℝ)⁻¹

-- ✅ CORRECT: Canonical form
calc (m:ℝ)⁻¹ * |∑...|    -- matches what simp produces

Why canonical forms matter: 1. Type matching: Integrable.of_bound and similar lemmas expect canonical forms 2. Consistency: All proofs use same notation 3. Avoids simp loops: Non-canonical forms may get simplified repeatedly

Canonical forms:

• Division: (m:ℝ)⁻¹ not 1/(m:ℝ) or ↑m⁻¹
• Coercion: (m:ℝ) not ↑m (when explicit)
• Norms: |x| not ‖x‖ after Real.norm_eq_abs

Common Calc Patterns

Triangle Inequality Chains

-- Common pattern for |a - c| ≤ |a - b| + |b - c|
intro ω  -- Use intro, not filter_upwards for simple pointwise
calc |f ω - h ω|
    _ = |f ω - g ω + (g ω - h ω)| := by ring_nf
  _ ≤ |f ω - g ω| + |g ω - h ω| := abs_add _ _
  _ ≤ ...

Sum Bound Chains

-- Pattern for bounding |(m:ℝ)⁻¹ * ∑ k, f k|
filter_upwards with ω; simp [Real.norm_eq_abs]
calc (m:ℝ)⁻¹ * |∑ k : Fin m, f k|
    _ ≤ (m:ℝ)⁻¹ * ∑ k : Fin m, |f k| := by
      gcongr; exact Finset.abs_sum_le_sum_abs _ _
  _ ≤ (m:ℝ)⁻¹ * ∑ k : Fin m, bound k := by
      gcongr with k; exact individual_bound k
  _ = ... := by ring

Gcongr in Calc

gcongr works seamlessly in calc chains for monotone operations:

calc (m:ℝ)⁻¹ * |∑ k, f k|
    _ ≤ (m:ℝ)⁻¹ * ∑ k, |f k| := by gcongr; exact sum_bound
  _ ≤ (m:ℝ)⁻¹ * (m * C) := by gcongr; exact term_bound

Anti-Patterns

❌ Redundant simp Steps in Calc

Don't manually perform what simp already did:

-- ❌ BAD
simp [Real.norm_eq_abs]
calc |(1/(m:ℝ)) * ∑...|
    = |(m:ℝ)⁻¹ * ∑...| := by rw [one_div]  -- simp already did this!
  _ = (m:ℝ)⁻¹ * |∑...| := by rw [abs_mul, abs_of_pos]; positivity  -- and this!

-- ✅ GOOD
simp [Real.norm_eq_abs]  -- Do simplifications once
calc (m:ℝ)⁻¹ * |∑...|   -- Start from result
  _ ≤ ...                -- Focus on actual reasoning

❌ Fighting Against Simp

If calc keeps failing, don't try to force it:

-- ❌ BAD: Adding rw to "fix" simp's transformations
simp [Real.norm_eq_abs]
calc |(1/(m:ℝ)) * ∑...|
    = ... := by rw [← one_div, ← Real.norm_eq_abs]; simp  -- fighting simp!

-- ✅ GOOD: Work with simp's transformations
simp [Real.norm_eq_abs]
calc (m:ℝ)⁻¹ * |∑...|  -- Accept simp's result
  _ ≤ ...

❌ Mixing Simplified and Unsimplified Forms

Be consistent within a calc chain:

-- ❌ BAD: mixing 1/(m:ℝ) and (m:ℝ)⁻¹
calc (m:ℝ)⁻¹ * |∑...|
    _ ≤ 1/(m:ℝ) * bound := ...  -- inconsistent notation!

-- ✅ GOOD: consistent notation
calc (m:ℝ)⁻¹ * |∑...|
    _ ≤ (m:ℝ)⁻¹ * bound := ...

Command Examples

Extended examples and session transcripts for Lean4 plugin commands.

---

draft

Skeleton-Only Drafting

```` User: /lean4:draft "Every continuous function on a compact set is bounded"

Claude: Parsing claim and drafting skeleton...

Theorem Skeleton

theorem continuous_on_compact_bounded
    {X : Type*} [TopologicalSpace X] [MetricSpace X]
    {Y : Type*} [MetricSpace Y]
    {K : Set X} (hK : IsCompact K)
    {f : X → Y} (hf : ContinuousOn f K) :
    IsBounded (f '' K) := by
  sorry

Elaboration check (--elab-check=best-effort)... ✓ (1 sorry, no other diagnostics)

What next?

• [alternative] Different formalization (e.g., using Bornology)
• [save to scratch] Write to scratch file

````

Attempt Mode

```` User: /lean4:draft --mode=attempt "The sum of two continuous functions is continuous"

Claude: Parsing claim and drafting skeleton...

theorem continuous_add {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) :
    Continuous (f + g) := by
  sorry

Attempting proof (--mode=attempt)... lean_local_search("Continuous add") → found Continuous.add Trying: exact hf.add hg Diagnostics... ✓

Proof found! Skeleton upgraded from sorry to verified proof.

What next?

• [show source] See the mathlib proof
• [alternative] Different formalization
• [save to scratch] Write to scratch file

````

---

formalize

Interactive Synthesis

```` User: /lean4:formalize "Every continuous function on a compact set is bounded"

Claude: ## Phase 1: Draft

Parsing claim and drafting skeleton...

theorem continuous_on_compact_bounded
    {X : Type*} [TopologicalSpace X] [MetricSpace X]
    {Y : Type*} [MetricSpace Y]
    {K : Set X} (hK : IsCompact K)
    {f : X → Y} (hf : ContinuousOn f K) :
    IsBounded (f '' K) := by
  sorry

Elaboration check... ✓ Attempting proof (--draft-mode=attempt)... lean_local_search("IsCompact ContinuousOn IsBounded image") → found it

Phase 2: Prove

Trying: exact hK.image_of_continuousOn hf |>.isBounded Diagnostics... ✓

Proof complete (--rigor=checked: no sorry, clean diagnostics, standard axioms).

What next?

• [show source] See the mathlib proof
• [alternative] Different formalization (e.g., using Bornology)
• [generalize] Weaken hypotheses
• [strengthen] Add conclusions
• [save to scratch] Write to scratch file

````

Axiomatic Draft

```` User: /lean4:formalize --rigor=axiomatic "The p-adic numbers are complete"

Claude: Drafting formalization with explicit assumptions...

namespace Assumptions

-- Assumption Ledger
-- ┌──────────────────────────────┬────────────────────────┬───────────┬─────────────────────┐
-- │ Assumption                   │ Justification          │ Scope     │ Introduced by       │
-- ├──────────────────────────────┼────────────────────────┼───────────┼─────────────────────┤
-- │ [MetricSpace (Padic p)]     │ standard p-adic metric │ instance  │ assistant-inferred  │
-- │ hp : Fact (Nat.Prime p)     │ p must be prime        │ parameter │ user-stated         │
-- └──────────────────────────────┴────────────────────────┴───────────┴─────────────────────┘

theorem padic_complete (p : ℕ) [hp : Fact (Nat.Prime p)] :
    CompleteSpace (Padic p) := by
  sorry -- ⚠ proof blocked: needs Mathlib.NumberTheory.Padics.PadicIntegers

bash "$LEAN4_SCRIPTS/check_axioms_inline.sh" <target>.lean --report-only → ✓ standard axioms only

Note: Mathlib likely has this as an instance. Searching... lean_leanfinder("CompleteSpace Padic") → Padic.instCompleteSpace

This is already a registered instance in mathlib. No axioms or assumptions needed.

What next?

• [show source] See how mathlib proves completeness
• [deeper] Explore the p-adic metric construction

````

---

prove

Basic Usage

/lean4:prove                         # Start guided session
/lean4:prove File.lean               # Focus on specific file
/lean4:prove --repair-only           # Fix build errors without filling sorries

Full Session Example

User: /lean4:prove

Claude: Discovering current state...

Using LSP:
- lean_diagnostic_messages(.) → 2 errors, 5 warnings
- lean_goal at each sorry → 8 goals to prove

## Prove Plan

**Found:** 8 sorries in 3 files
**Approach:** Balanced
**Review:** Every 5 changes

### Sorries Found
- `Helpers.lean:15` - in `trivial_lemma`
- `Helpers.lean:42` - in `helper_bound`
- `Core.lean:89` - in `main_theorem`
...

**Proceed?** (yes / adjust / cancel)

User: yes

Claude: Working on Helpers.lean:15 - `trivial_lemma`...

Goal: ⊢ 0 ≤ 1

Searching mathlib... Found: `Nat.zero_le`

Applying: `exact Nat.zero_le 1`
Building... ✓

Committing: "fill: trivial_lemma - exact Nat.zero_le"

[continues for each sorry...]

Repair Mode Example

User: /lean4:prove --repair-only

Claude: Running repair mode...

Build errors found:
- Core.lean:42: type mismatch at application
- Core.lean:89: unknown identifier 'continuous_of_foo'

Repairing Core.lean:42...
Error: type mismatch, expected `ℕ`, got `ℤ`
Fix: Adding coercion with `↑`
Building... ✓

Repairing Core.lean:89...
Searching mathlib for 'continuous_of_foo'...
Found: `Continuous.comp` in Mathlib.Topology.Basic
Fix: Replacing with correct lemma name
Building... ✓

## Repair Complete
- Errors fixed: 2/2
- Build status: ✓ passing

Review Checkpoint Example

## Progress

**Filled:** 5/8 sorries
**Commits:** 5 new
**Build:** passing

**Current:** Core.lean:89 - `main_theorem`
**Status:** Searching mathlib...

**Options:**
- `continue` - Keep going
- `stop` - Save progress and exit
- `skip` - Skip current sorry, try next
- `rollback N` - Undo last N commits

---

autoformalize

Basic Usage

/lean4:autoformalize --source ./paper.pdf --claim-select=first --out=Paper.lean
/lean4:autoformalize --source ./paper.pdf --claim-select=regex:"Theorem.*" --out=Paper.lean --rigor=checked

Full Session Example

User: /lean4:autoformalize --source ./paper.pdf --claim-select=first --out=Paper.lean

Claude: Extracting claims from ./paper.pdf...
Found 4 claims in document order:
  1. Theorem 2.1 (Continuity bound)
  2. Lemma 2.3 (Monotone helper)
  3. Theorem 3.1 (Main convergence)
  4. Corollary 3.2 (Uniform bound)

Applying --claim-select=first → queue: [Theorem 2.1]

[Synthesis — Claim 1/1: Theorem 2.1]
Drafting "Theorem 2.1"...
  draft → temp file (declaration-only block, fully-qualified names)
  Outer loop: append to Paper.lean with boundary marker
  lean_diagnostic_messages(Paper.lean) → ✓
  Committing: "draft: Theorem 2.1 continuity bound"

Starting inner cycle on Paper.lean...
[Cycle 1] Working on Paper.lean:18 - `continuity_bound`
  Goal: ⊢ ∀ x ∈ K, ‖f x‖ ≤ C
  lean_leanfinder("IsCompact ContinuousOn norm bound") → found candidate
  Applying: `exact hK.isCompact.norm_le_of_continuousOn hf` ✓
  Committing: "fill: continuity_bound - isCompact.norm_le"

Sorry-free. Queue empty.

## Autoformalize Summary

**Reason stopped:** queue-empty (all claims attempted)

| Metric | Value |
|--------|-------|
| Claims attempted | 1/1 |
| Sorries before | 0 |
| Sorries after | 0 |
| Cycles run | 1 |
| Stuck cycles | 0 |
| Deep invocations | 0 |
| Time elapsed | 3m |
| Drafts | 1 |

**Handoff recommendations:**
- All sorries filled. Run /lean4:checkpoint to save.

---

autoprove

Basic Usage

/lean4:autoprove                        # Start autonomous session
/lean4:autoprove File.lean              # Focus on specific file
/lean4:autoprove --max-cycles=10        # Limit total cycles

Full Session Example

User: /lean4:autoprove

Claude: Discovering current state...

Using LSP:
- lean_diagnostic_messages(.) → 2 errors, 5 warnings
- lean_goal at each sorry → 8 goals to prove

Starting autonomous loop (max-cycles=20, max-stuck=3)...

[Cycle 1] Working on Helpers.lean:15 - `trivial_lemma`...
Goal: ⊢ 0 ≤ 1
Applying: `exact Nat.zero_le 1` ✓
Committing: "fill: trivial_lemma - exact Nat.zero_le"

[Cycle 1] Working on Helpers.lean:42 - `helper_bound`...
Goal: ⊢ a + b ≤ b + a
Applying: `linarith` ✓
Committing: "fill: helper_bound - linarith"

Checkpoint: 2 sorries filled, build passing ✓
Review: No blockers found, continuing...

[Cycle 2] Working on Core.lean:89 - `main_theorem`...
Stuck: Same error after 2 attempts
Running stuck review...
Replanning: Search Mathlib.Topology.Order for tendsto variants
[continues autonomously...]

See cycle-engine.md for stuck detection logic and deep mode for escalation behavior.

Stop Condition Example

## Autoprove Summary

**Reason stopped:** max-stuck (3 consecutive stuck cycles)

| Metric | Value |
|--------|-------|
| Sorries before | 8 |
| Sorries after | 3 |
| Cycles run | 7 |
| Stuck cycles | 3 |
| Deep invocations | 2 |
| Time elapsed | 45m |

**Handoff recommendations:**
- Run /lean4:prove for guided work on remaining 3 sorries
- Review stuck blockers: Core.lean:89, Core.lean:156, Bounds.lean:42

Deep Rollback Example

[Cycle 4] Working on Core.lean:89 - `main_theorem`...
Stuck after 3 attempts. Escalating to deep mode (--deep=stuck)...

Creating snapshot (--deep-snapshot=stash)...
Snapshot captured: <snapshot-id>

Deep phase 1: Extracting helper lemma to Helpers.lean
  Compile: ✓ (sorry count: 1 → 1, no new diagnostics)
Deep phase 2: Filling sorry using helper
  Compile: ✗ — sorry count increased (1 → 3)

Regression detected (--deep-regression-gate=strict):
  Sorry count: 1 → 3 (+2 regression)
  Rolling back to <snapshot-id>...
  Rollback: ✓
  Marking stuck: "deep: regression — sorry count increased from 1 to 3"

Stuck handoff:
- Deep abort reason: regression (sorry count +2)
- Strategy attempted: helper extraction to Helpers.lean
- LSP queries: lean_leanfinder("convergence bound"), lean_local_search("tendsto")
- Recommendation: try alternative approach or manual guidance

Running stuck review...

Note: if rollback itself fails, the cycle stops immediately —
no checkpoint is created, and the sorry is marked stuck with
"deep: rollback failed".

Edge case — new diagnostic errors (sorry count unchanged):

Deep phase 1: Refactoring Filter usage in Core.lean
  Compile: sorry count 1 → 1, but 2 new type mismatch errors

Regression detected (--deep-regression-gate=strict):
  New diagnostics: 2 errors not present in pre-deep baseline
  Rolling back to <snapshot-id>...
  Marking stuck: "deep: regression — new errors"

---

checkpoint

Basic Usage

/lean4:checkpoint
/lean4:checkpoint "optional custom message"

Full Session Example

User: /lean4:checkpoint

Claude: Creating checkpoint...

Compiling touched files...
✓ MyProject/Basic.lean compiled
✓ MyProject/Lemmas.lean compiled

Building project...
✓ lake build passed

Checking axioms...
✓ Standard axioms only (propext, Classical.choice)

Counting sorries...
→ 3 sorries remaining in 2 files

Staging changes...
→ 5 files modified

Creating commit...
✓ Commit a1b2c3d: checkpoint(lean4): 3 sorries remaining, build passing

## Checkpoint Created

Commit: a1b2c3d - checkpoint(lean4): 3 sorries remaining, build passing
Build: ✓ passing
Sorries: 3 remaining
Axioms: standard only

Next steps:
- Continue with /lean4:prove
- Push manually when ready: git push

Rollback Examples

# Undo last commit, keep changes staged
git reset --soft HEAD~1

# Undo last commit, keep changes unstaged
git reset HEAD~1

# Undo last N commits
git reset HEAD~N

---

review

Basic Usage

/lean4:review                        # Review changed files (default)
/lean4:review File.lean              # Review specific file
/lean4:review File.lean --line=89    # Review single sorry
/lean4:review --scope=project        # Review entire project (prompts)

Full Review Example

User: /lean4:review Core.lean

Claude: Running review on Core.lean...

## Lean4 Review Report
**Scope:** Core.lean (file — target default)

### Build Status
✓ Core.lean compiles successfully

### Sorry Audit (1 remaining)
- Core.lean:89 - `convergence_bound`
  Goal: `∀ ε > 0, ∃ N, ∀ n ≥ N, |f n - L| < ε`
  Suggestion: Search mathlib for `Metric.tendsto_atTop`

### Axiom Status
✓ Standard axioms only

### Style Notes
- Line 45: Consider `simp only [add_comm, mul_comm]` instead of `simp [*]`
- Line 78: Proof is 38 lines - consider extracting helper lemma

### Golfing Opportunities
- Line 23: `apply f; exact h` → `exact f h` (directness win)
- Line 56: `ext x; simp` - verify if `simp` alone suffices

### Complexity Summary
- Theorems in file: 8
- Average proof: 15 lines
- Longest: `convergence_bound` (38 lines)

### Recommendations
1. Fill `convergence_bound` sorry - likely in mathlib
2. Extract helper from long proof at line 78
3. Tighten `simp` calls for faster compilation

External Tool Integration Example

User: /lean4:review Core.lean --codex

Claude: Running review with Codex integration...

## Lean4 Review Report

### Build Status
✓ Core.lean compiles

### Sorry Audit
- Line 89: `convergence_bound` - needs proof

### Codex Suggestions
- Line 89: "Search Mathlib for `tendsto_atTop` variants — goal shape matches convergence lemmas"
- Line 45: "Broad `simp` may slow compilation — consider narrowing to specific lemmas"

### Claude Analysis
[standard review sections...]

Custom Hook Interface

See review-hook-schema.md for full input/output schemas and example scripts.

Stuck Review Example

See cycle-engine.md for stuck detection criteria.

[Autoprove detects no progress on Core.lean:89]

Claude: No progress on Core.lean:89 after 3 attempts. Running stuck review...

## Stuck Review — Core.lean:89

**Top 3 blockers:**
1. Missing lemma for tendsto_atTop → search Mathlib.Topology.Order
2. Need MeasurableSpace instance → add `haveI` before apply
3. Goal has implicit coercion issue → try `convert` instead of `exact`

**Recommended:** Search tendsto variants first.

Review complete. Proposed plan:
1. Search Mathlib.Topology.Order for tendsto_atTop variants
2. Add `haveI : MeasurableSpace β := inferInstance` before apply
3. If exact fails, try `convert` with explicit type annotation

Proceed with this plan? [yes / no / skip]

User: yes

Claude: Continuing with plan...

End-of-Session Golf Example

## Session Complete

Filled: 5/8 sorries
Commits: 5 new

Create checkpoint? (per-file + project build, axiom check, commit)
- [yes] — run /lean4:checkpoint
- [no] — keep commits as-is

User: yes

Claude: Running checkpoint... ✓

Run /lean4:golf on touched files?
Files modified: Core.lean, Helpers.lean
- [yes] — golf each file
- [no] — skip

User: yes

Claude: Golfing Core.lean...
[golf output]

Counterexample Discovery Example

See cycle-engine.md for artifact templates.

Claude: Working on Core.lean:42 - `naive_bound`...

Goal: ⊢ ∀ n : Fin 5, n.val < 3

Preflight falsification (Fin 5 is decidable)...
Trying decide... Found counterexample: n = 3

## Counterexample Found

Statement `naive_bound` is false.
Witness: `⟨3, by decide⟩` with `¬ (3 < 3)`

Creating counterexample lemma...

/-- Counterexample to naive_bound -/ theorem naive_bound_counterexample : ∃ n : Fin 5, ¬ (n.val < 3) := by exact ⟨3, by decide⟩

Create salvage lemma? [yes/no]

User: yes

Claude: What correction makes it true?
- Option A: Restrict domain to `Fin 3` (all values < 3)
- Option B: Weaken bound to `n.val < 5` (trivially true for `Fin 5`)

User: A

Creating salvage:

/-- Salvaged version of naive_bound: restrict to Fin 3 -/ theorem naive_bound_salvaged : ∀ n : Fin 3, n.val < 3 := by intro n; exact n.isLt

Committing: "disprove: naive_bound - counterexample at n=3"

---

File Verification

Three-Tier Verification Ladder

Use the lightest tool that answers the question:

Run lake env lean from the Lean project root; pass repo-relative file paths.

Anti-Pattern: lake build with File Arguments

# ✗ Wrong — lake build does not accept file path arguments
lake build InfinitaryLogic/Scott/Sentence.lean
→ error: unknown target 'InfinitaryLogic/Scott/Sentence.lean'

# ✓ Correct — use lake env lean for single-file compilation
lake env lean InfinitaryLogic/Scott/Sentence.lean
→ (compiles single file with lake environment)

Typical Verification Flow

1. Edit proof
2. lean_diagnostic_messages(file)    # immediate feedback
3. Fix any issues
4. lake env lean path/to/File.lean   # file-level gate (from project root)
5. Continue editing...
6. lake build                        # project gate at checkpoint only

---

refactor

Basic Usage

User: /lean4:refactor ForwardEuler/Main.lean

## Refactor Plan — ForwardEuler/Main.lean

### Strategy Improvements
1. `continuousOn_eulerPath` (line 104): case-splitting on endpoints
   → Use `ContinuousOn.congr` + `Set.EqOn` (saves ~20 lines)

2. `hasDerivWithinAt_eulerPath` (line 149): manual derivative via unfolding
   → Use `HasDerivAt` chain + `congr_of_eventuallyEq` (saves ~5 lines)

### Helper Extraction
1. Floor computation from Ico membership — appears 4x (lines 89, 119, 155, 198)
   → Extract `floor_eq_of_mem_Ico`

### Estimated Impact
- Lines before: 310
- Lines after: ~245
- Helpers extracted: 1
- Mathlib lemmas newly applied: 3

Apply batch 1 (3 changes)? [yes / skip / stop]

Dry Run

User: /lean4:refactor --scope=changed --dry-run

Reports opportunities without editing files.

---

golf

Basic Usage

/lean4:golf                     # Golf entire project
/lean4:golf File.lean           # Golf specific file
/lean4:golf File.lean:42        # Golf proof at specific line
/lean4:golf --dry-run           # Show opportunities without applying

Full Session Example

User: /lean4:golf Core.lean

Claude: Verifying build...
✓ Core.lean compiles

Finding golfing opportunities...

Found 7 patterns:
- 3 directness wins (ext+rfl, apply+exact, constructor+exact)
- 1 performance cleanup (simp narrowing)
- 1 safe inline (let used once)
- 1 skip (let used 5 times)
- 1 skip (rwa replacement — marginal)

Applying optimizations...

[1/6] Line 45: ext x; rfl → rfl (directness)
  Diagnostics... ✓

[2/6] Line 66: apply f; exact h → exact f h (directness)
  Diagnostics... ✓

[3/6] Line 112: constructor; exact; exact → exact ⟨_, _⟩ (directness)
  Diagnostics... ✓

[4/6] Line 34: simp [...] → simp only [...] (performance)
  Diagnostics... ✓

[5/6] Line 67: Inline let bound := ...
  Checking usage... 1 reference, safe
  Diagnostics... ✓

[6/6] Line 23: rw [h]; exact → rwa [h]
  Skipped: only 1-line win, moves up tactic complexity ladder (rw+exact → rwa)

## Golf Results

Meaningful simplifications: 3 (directness improvements)
Performance cleanups: 1 (simp narrowing)
Syntax cleanups: 1 (let inline)
Skipped: 2 (1 safety — let used 5×, 1 marginal — rwa replacement)
Build status: ✓ passing
Total savings: 6 lines (~9%)

Dry Run Example

User: /lean4:golf --dry-run

Claude: Scanning for opportunities...

## Golf Opportunities (Dry Run)

**File:** Core.lean

| Line | Pattern | Benefit | Confidence | Savings |
|------|---------|---------|------------|---------|
| 78 | ext + rfl → rfl | Directness | High | 1 line |
| 45 | Inline let (1 use) | Clarity | High | 2 lines |
| 34 | simp → simp only | Performance | High | 0 lines |
| 56 | Inline let (4 uses) | — | Skip | - |
| 23 | rw + exact → rwa | Marginal | Skip | 1 line |

**Estimated savings:** 3 lines from 3 safe optimizations (+ 1 perf-only)
**Run without --dry-run to apply**

Saturation Example

## Golf Results

**File:** Core.lean
**Optimizations applied:** 12
**Build status:** ✓ passing

Saturation reached after 12 optimizations.
Remaining 3 opportunities are false positives or low-value.

Success rate dropped to 15% (below 20% threshold).
Recommend stopping further golfing on this file.

Taste-Driven Golfing Example

User: /lean4:golf Analysis.lean

Claude: Verifying build...
✓ Analysis.lean compiles

Finding golfing opportunities...

Found 8 patterns (4 actionable, 4 skipped)

[1/4] Line 23: apply f; exact h → exact f h (directness)
  Diagnostics... ✓

[2/4] Line 45: simp [h1, h2, h3] → simp only [h1, h2] (performance — linter flagged h3 unused)
  Diagnostics... ✓

[3/4] Line 67: rw [h]; exact trivial → rwa [h]
  Skipped: 1-line win but moves up tactic complexity ladder (rw+exact is explicit,
  rwa is heavier automation). Not worth surfacing.

[4/4] Line 89: 3-line proof → 1 line with <;>
  cases h with | inl => simp [ha] | inr => simp [hb]
  Candidate: cases h <;> simp [ha, hb]
  Skipped: branches use different simp arguments — <;> only for literally identical goals

[5/4] Line 102: simpa using h_bound → exact h_bound
  Diagnostics... ✓ (simpa does no actual simplification here — exact is more direct)

[6/4] Line 115: 2-line proof kept as-is
  have h_key := critical_step a b
  exact h_key.trans (by ring)
  Candidate 1-line: exact (critical_step a b).trans (by ring)
  Skipped: named intermediate `h_key` has semantic value, 1-line form is more opaque

## Golf Results

Meaningful simplifications: 2 (directness improvements)
Performance cleanups: 1 (simp narrowing)
Skipped: 3 (1 tactic complexity, 1 non-identical <;>, 1 semantic name preserved)
Build status: ✓ passing
Total savings: 3 lines (~5%)

Search Mode Example

User: /lean4:golf Core.lean --search=quick

Claude: Verifying build...
✓ Core.lean compiles

Finding golfing opportunities...
Found 4 syntactic patterns + 2 lemma replacement candidates

[1/6] Line 23: apply f; exact h → exact f h (directness)
  Diagnostics... ✓

[2/6] Line 30: custom_continuous_comp → Continuous.comp (mathlib)
  LSP search: lean_local_search("continuous comp")
  Testing replacement... ✓ (1/2 candidates passed)
  Import: Mathlib.Topology.Basic
  Diagnostics... ✓

[3/6] Line 45: Inline let (1 use)
  Diagnostics... ✓

[4/6] Line 67: custom_bound_lemma → replacement candidate
  LSP search: lean_leanfinder("bound monotone")
  Testing replacement... ✗ type mismatch (0/2 passed)
  Skipped (hand off to axiom-eliminator for deeper work)

## Golf Results

Optimizations applied: 3/6
Replacements: 1 lemma (mathlib)
Skipped: 1 (safety), 1 (needs axiom-eliminator)
Total savings: 5 lines (~8%)
Build status: ✓ passing

Delegation Preflight Failure Example

User: /lean4:golf --max-delegates=3

Claude: Verifying build...
✓ Project compiles

Running preflight: delegating Core.lean:23 to golfer subagent...

⚠ Preflight subagent hit Edit permission prompt.
Stopping delegation immediately — switching to direct mode.

Continuing in main agent (no subagents will be launched)...

[1/6] Line 23: apply f; exact h → exact f h (directness)
  Diagnostics... ✓

[2/6] Line 45: ext x; rfl → rfl (directness)
  Diagnostics... ✓

[continues directly without delegation...]

Bulk Rewrite Auto-Revert Example

User: /lean4:golf Core.lean

Claude: Verifying build...
✓ Core.lean compiles

Finding golfing opportunities...
Found 8 `:= by exact` candidates in declaration RHS positions (≥4 → bulk mode)

Preview (3 of 8):
  Line 23: `:= by exact h` → `:= h`
  Line 67: `:= by exact rfl` → `:= rfl`
  Line 101: `:= by exact Nat.zero_le 1` → `:= Nat.zero_le 1`

Apply as batch? [yes / individual / skip]

User: yes

Capturing baseline diagnostics...
Baseline: 0 diagnostics, 0 sorries

Applying batch (8 replacements, Core.lean)...
Running lean_diagnostic_messages(Core.lean)...

⚠ Regression detected:
  - 2 new diagnostics (type mismatch at lines 45, 89)
  - Sorry count: 0 → 0 (unchanged)

Restoring from pre-batch snapshot...
✓ Core.lean restored to pre-batch state

Falling back to individual edits...
[1/8] Line 23: `:= by exact h` → `:= h`
  Diagnostics... ✓
[2/8] Line 45: `:= by exact rfl` — skipped (calc block context)
[3/8] Line 89: `:= by exact (by ring)` — skipped (nested tactic-mode boundary)

Applied 5/8, skipped 2 (context rules), reverted 1 (regression)

Context-Ambiguous Skip Example

User: /lean4:golf Lemmas.lean

Claude: Finding golfing opportunities...

Found 5 `:= by exact` candidates

[1/5] Line 12: `:= by exact h`
  Context: declaration RHS ✓, no nested tactic boundary ✓
  Diagnostics... ✓

[2/5] Line 34: `:= by exact (by simp)`
  Skipped: nested tactic-mode boundary in TERM

[3/5] Line 56: inside `calc` block
  Skipped: disallowed context (calc)

[4/5] Line 78: uncertain elaboration context
  Skipped: context classification uncertain — never force

Applied 3/5, skipped 2 (context rules)

Exact-Collapse Example

```` User: /lean4:golf Core.lean --search=quick

Claude: Verifying build... ✓ Core.lean compiles

Finding golfing opportunities... Running: find_golfable.py Core.lean --patterns apply-exact-chain --filter Found 6 apply-exact-chain anchors

[1/6] Line 34: Mechanical collapse apply mul_lt_mul_of_pos_right; · exact h_bound; · exact h_pos → exact mul_lt_mul_of_pos_right h_bound h_pos lean_multi_attempt... ✓ Diagnostics baseline check... ✓ (no new diagnostics, sorry count unchanged)

[2/6] Line 52: Mechanical collapse apply HasDerivAt.div; · exact hf; · exact hg → exact hf.div hg lean_multi_attempt... ✓ Diagnostics baseline check... ✓

[3/6] Line 71: Readability skip apply f; · apply g; · apply h; · exact a; · exact b Collapsed form: exact f (g (h a b)) — >2 nesting depth, marginal net win Skipped (readability)

[4/6] Line 89: Mechanical collapse apply Continuous.comp; · exact continuous_neg; · exact hf → exact continuous_neg.comp hf lean_multi_attempt... ✓ Diagnostics baseline check... ✓

[5/6] Line 103: Skipped (inside cases block)

[6/6] Line 115: Exploratory probe (--search=quick) apply bound_mono; · exact h_le; · exact h_pos Candidate 1: exact bound_mono h_le h_pos — lean_multi_attempt ✗ Candidate 2: exact h_le.bound_mono h_pos — lean_multi_attempt ✓ Diagnostics baseline check... ✓

Golf Results

Exact-collapse: Mechanical 3 applied, Exploratory 1 found. Skipped: 1 (readability), 1 (unsafe context) Total savings: 8 lines (~15%) Build status: ✓ passing ````

---

learn

Repo Mode — Exploring Project Structure

User: /lean4:learn --mode=repo --scope=project

Claude: Scanning project structure...

Found 12 .lean files across 3 directories.

## Project Map

├── InfinitaryLogic/
│   ├── Basic.lean          — Core definitions (Language, Term, Formula)
│   ├── Semantics.lean      — Model theory (Structure, Interpretation)
│   └── Scott/
│       ├── Sentence.lean   — Scott sentences (4 sorries)
│       └── Isomorphism.lean — Back-and-forth (2 sorries)
├── Helpers/
│   ├── Ordinal.lean        — Ordinal utilities (complete)
│   └── Cardinal.lean       — Cardinal bounds (1 sorry)
└── lakefile.lean

Key dependency flow:
  Basic → Semantics → Scott/Sentence → Scott/Isomorphism
  Helpers/Ordinal → Scott/Sentence

What would you like to explore?
- [deeper] Drill into a specific file
- [deps] Show full dependency graph
- [sorries] Focus on the 7 remaining sorries

Mathlib Mode — Navigating a Topic

```` User: /lean4:learn --mode=mathlib topology compact

Claude: Searching mathlib for compactness in topology...

lean_local_search("compact topology") → 12 results lean_leanfinder("IsCompact") → 8 results

Compactness in Mathlib

Core definition: IsCompact in Mathlib.Topology.Defs.Basic

def IsCompact (s : Set α) : Prop :=
  ∀ ⦃f : Filter α⦄, NeBot f → f ≤ 𝓟 s →
    ∃ a ∈ s, ClusterPt a f

Key lemmas:

Hierarchy: TopologicalSpace → CompactSpace → IsCompact (for subsets)

What next?

• [show proof] See proof of a specific lemma
• [related] Explore related concepts (sequentially compact, totally bounded)
• [alternative] See filter-free characterization

````

Game Style — Natural Numbers Track

```` User: /lean4:learn --style=game --track=nng-like

Claude: [Intent: usage (inferred) | Presentation: formal]

Starting Natural Numbers Game — Track: nng-like (8 levels)

Level 1: Zero + n = n

Prove that 0 + n = n for all natural numbers n.

theorem zero_add (n : Nat) : 0 + n = n := by
  sorry

Hint available if you need it. Type your proof:

User: induction n with | zero => rfl | succ n ih => simp [Nat.add_succ, ih]

Claude: Verifying via lean_goal + lean_multi_attempt... lean_diagnostic_messages → clean ✓ Level 1 complete! [verified]

Level 2: Succ (a + b) = a + Succ b

theorem succ_add (a b : Nat) : Nat.succ a + b = Nat.succ (a + b) := by
  sorry

[continue / skip / quit] ````

Paper as Source — Math Intent

```` User: /lean4:learn --source ./papers/stone-weierstrass.pdf

Claude: Reading PDF... extracting key results.

[Intent: math (inferred from PDF) | Presentation: informal]

Stone–Weierstrass: Main Results [unverified]

1. Theorem 1 (Real): If A is a subalgebra of C(X, ℝ) that separates points and contains constants, then A is dense in C(X, ℝ). 2. Theorem 2 (Complex): The analogous result for self-adjoint subalgebras of C(X, ℂ). 3. Corollary: Every continuous function on [a,b] is a uniform limit of polynomials (Weierstrass).

Which result would you like to explore?

User: 1

Claude: Theorem 1 says that polynomial-like function algebras are "enough" to approximate any continuous function, provided two conditions...

[explains conceptually at user's level]

Want to see this formalized in Lean to make it concrete?

[deeper / show source / formalize → /lean4:formalize] ````

---

doctor

Basic Usage

/lean4:doctor              # Full diagnostic
/lean4:doctor env          # Environment only
/lean4:doctor migrate      # Migration assistance
/lean4:doctor cleanup      # Remove obsolete files

Full Diagnostic Example

User: /lean4:doctor

Claude: Running diagnostics...

## Lean4 Doctor Report

### Environment
✓ lean 4.15.0
✓ lake 4.15.0
✓ python3 3.11.2
✓ git 2.43.0
✓ rg 14.1.0

### MCP Tools
✓ Lean LSP MCP tools available in this session (lean_goal)

### Plugin
✓ LEAN4_PLUGIN_ROOT=/home/user/.claude/plugins/lean4
✓ LEAN4_SCRIPTS=/home/user/.claude/plugins/lean4/lib/scripts
✓ Hooks executable
✓ Scripts executable (12 files)

### Project
✓ lakefile.lean found
✓ lean-toolchain: leanprover/lean4:v4.27.0
✓ Build passes
→ 3 sorries in Core.lean

### Migration
✓ Clean installation (no v3 artifacts)

### Status: Ready

Your environment is configured correctly.
Run /lean4:prove to fill the 3 remaining sorries.

Migration Example

User: /lean4:doctor migrate

Claude: Checking for v3 artifacts...

Found v3 installation:
- .claude/tools/lean4/ (12 files)
- .claude/docs/lean4/ (8 files)

## Migration Steps

1. Uninstall old plugins:
   /plugin uninstall lean4-theorem-proving
   /plugin uninstall lean4-memories
   /plugin uninstall lean4-subagents

2. Install unified plugin:
   /plugin marketplace add cameronfreer/lean4-skills
   /plugin install lean4

3. Optional cleanup:
   rm -rf .claude/tools/lean4 .claude/docs/lean4

Proceed with migration? (yes/no)

Cleanup Example

User: /lean4:doctor cleanup

Claude: Scanning for obsolete files...

Found:
- .claude/tools/lean4/ (12 files, 45KB)
- .claude/docs/lean4/ (8 files, 32KB)

These are v3 artifacts that are no longer needed.
Remove them? (yes/no)

User: yes

Claude: Removing .claude/tools/lean4/... ✓
Removing .claude/docs/lean4/... ✓

Cleanup complete. 77KB freed.

Command Invocation Contract

This plugin ships a host-agnostic parser (lib/command_args/) that covers the parser-decidable startup rules of the six parameter-heavy commands — draft, learn, formalize, autoformalize, prove, and autoprove. Parser-decidable rules are those whose outcome can be fully determined from flags, positionals, and os.path.exists checks alone, without repo-level search or interactive user prompting. A small set of documented startup rules in these commands depend on runtime context the parser cannot evaluate (e.g. local-declaration resolution in learn); those are listed in the forward- exclusions and are applied by the command at runtime after reading the parser's output. Other commands in this plugin (checkpoint, review, refactor, golf, doctor) are not parameter-heavy and are not covered by lib/command_args/; they remain model-parsed on every host.

For the six covered commands, whether the parser actually runs before the model sees a slash-command invocation depends on the host adapter:

• The Claude Code adapter invokes the parser from a UserPromptSubmit

hook before the model sees the prompt and rejects invalid invocations with a hook-level block.

• Other host adapters MAY invoke the same parser via

lib/scripts/parse_command_args.py. Hosts that do not integrate the parser fall back to the model-parsed Required Startup Behavior below — on those hosts, slash-command inputs remain model-parsed.

Regardless of host or command, the plugin does not enforce wall-clock budgets on the plugin's behalf — those remain best-effort and are re-checked at safe boundaries by the command itself.

Required Startup Behavior

Any command that advertises flags must do all of the following before substantive work:

1. Parse the raw invocation text against the command's documented input table. 2. Emit a Resolved Inputs summary showing:

• explicit values supplied by the user
• defaults that were assumed
• coercions or ignored flags
• startup validation errors

3. Refuse to start on startup validation errors. Do not partially begin a session and then discover a missing required companion flag later. 4. Maintain promised session counters explicitly (cycles_run, stuck_cycles, deep_invocations, and similar state) rather than relying on the model to remember them informally.

Validated Invocation Block (host-provided)

A host adapter MAY pre-parse a slash-command invocation and inject the result into the model's context as a fenced validated-invocation block. The block is a lossless serialization of the host parser's ParseResult.

When such a block appears in context for the current /lean4:<command> invocation, the command MUST treat it as the authoritative interpretation of parser-decidable inputs and MUST NOT re-parse the raw invocation text for those inputs.

Commands that have repo-dependent startup rules — rules whose outcome depends on runtime context the host parser cannot evaluate — MAY apply those rules after reading the block, refining specific fields with runtime context. The command's emitted Resolved Inputs summary may differ from the block for forward-excluded fields only; for all parser-decided fields, the Resolved Inputs MUST match the block exactly.

When no validated-invocation block appears (non-Claude hosts, or hosts that have not installed the parser hook), the command falls back to the Required Startup Behavior above and parses the raw text itself.

A validated-invocation block carrying any startup-validation error never reaches the model: the host adapter rejects the prompt before invocation. A block carrying only warnings reaches the model and the command surfaces those warnings in its Resolved Inputs summary.

Adapter Implementations

• Default (model-parsed): non-Claude hosts pass the raw tail to the model;

the command parses it per the Required Startup Behavior above.

• Claude plugin (hook-validated): the UserPromptSubmit hook

hooks/validate_user_prompt.py parses /lean4:* prompts via lib/command_args/ before the model sees them. Hard errors are returned to the user as a hook rejection; successful parses are injected as a validated-invocation block. Other hosts can call the same parser via lib/scripts/parse_command_args.py.

Enforcement Classes

Document each flag according to the strongest guarantee the current architecture can actually provide:

• Startup-validated: syntax, enums, required companion flags, path safety,

overwrite checks, and other checks that can be decided before work starts.

• Session-enforced: counters and mode switches that the command re-checks at

safe boundaries during the session.

• Best-effort: budgets that depend on wall-clock time or other values the

host does not enforce. These must be checked explicitly by the command, but they are not kill switches.

• Advisory: preferences that guide planning or presentation but are not

safety or stop guarantees.

Never describe a best-effort control as a hard stop.

Wall-Clock Budgets

--max-total-runtime is the clearest example of a best-effort control:

• record a start timestamp before the main loop begins
• re-check elapsed wall-clock time with date +%s (or equivalent) at cycle

boundaries and before expensive optional branches such as deep mode

• stop before starting the next unit of work when the budget has been exhausted

Do not claim that --max-total-runtime can preempt a long-running tool call mid-step. The host does not provide that guarantee here.

Common Compilation Errors in Lean 4

This reference provides detailed explanations and fixes for the most common compilation errors encountered in Lean 4 theorem proving.

Quick Reference Table

---

⚡ WORKING WITH SUB-σ-ALGEBRAS?

If you're defining multiple `MeasurableSpace` instances (sub-σ-algebras), STOP and read this first:

📚 [instance-pollution.md](instance-pollution.md) - Essential guide to prevent:

• Subtle bugs: Lean picks wrong instance (even from outer scopes!)
• Timeout errors: 500k+ heartbeat explosions
• Cryptic errors: "synthesized: m, inferred: inst✝⁴"

Quick fix: Pin ambient instance BEFORE defining sub-σ-algebras (see instance-pollution.md for details).

---

Detailed Error Explanations

1. Failed to Synthesize Instance

Full error message:

failed to synthesize instance
  IsProbabilityMeasure μ

What it means: Lean cannot automatically infer the required type class instance.

Common scenarios:

• Working with sub-σ-algebras: m ≤ m₀ but Lean can't infer instances on m
• Trimmed measures: μ.trim hm needs explicit SigmaFinite instance
• Conditional expectations requiring multiple measure properties

Solutions:

Pattern 1: Explicit instance declaration

haveI : IsProbabilityMeasure μ := ⟨measure_univ⟩
haveI : IsFiniteMeasure μ := inferInstance
haveI : SigmaFinite (μ.trim hm) := sigmaFinite_trim μ hm

Pattern 2: Using Fact for inequalities

have h_le : m ≤ m₀ := ...
haveI : Fact (m ≤ m₀) := ⟨h_le⟩

Pattern 3: Explicit instance passing

@condExp Ω ℝ m₀ m (by exact inst) μ (by exact hm) f

Pattern 4: Exclude unwanted section variables

-- When section has `variable [MeasurableSpace Ω]` but lemma doesn't need it
omit [MeasurableSpace Ω] in
/-- Docstring for the lemma -/
lemma my_lemma : Statement := by
  proof

• Must appear before the docstring (not after)
• Common when section variables cause unwanted instance requirements
• Can omit multiple: omit [inst1] [inst2] in

⚡ CRITICAL for sub-σ-algebras: If working with multiple MeasurableSpace instances, read [instance-pollution.md](instance-pollution.md) FIRST to avoid subtle bugs and timeout errors!

For deep patterns with sub-σ-algebras, conditional expectation, and measure theory type class issues, see: measure-theory.md

Debug with:

set_option trace.Meta.synthInstance true in
theorem my_theorem : Goal := by
  apply_instance

2. Maximum Recursion Depth

Full error message:

(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached

What it means: Type class synthesis is stuck in a loop or the search is too complex.

Common causes:

• Circular instance dependencies
• Very deep instance search trees
• Ambiguous instances competing

Solutions:

Solution 1: Provide instance manually

letI : MeasurableSpace Ω := m₀  -- Freeze the instance
-- Now Lean won't search

Solution 2: Increase search limit

set_option synthInstance.maxHeartbeats 40000 in
theorem my_theorem : Goal := ...

Solution 3: Check for instance loops

-- ❌ WRONG: Creates loop
instance [Foo A] : Bar A := ...
instance [Bar A] : Foo A := ...

-- ✅ CORRECT: One-directional
instance [Foo A] : Bar A := ...

3. Type Mismatch

Full error message:

type mismatch
  x
has type
  ℕ
but is expected to have type
  ℝ

What it means: The term's type doesn't match what's expected.

Common scenarios:

• Natural number used where real number expected
• Integer used where rational expected
• General coercion needed

Solutions:

Pattern 1: Explicit coercion

-- Natural to real
(n : ℝ)  -- Preferred
↑n       -- Alternative

-- Integer to real
(z : ℝ)

-- Custom coercion
⟨x, hx⟩ : {x : ℝ // x > 0}

Pattern 2: Check actual types

#check x        -- See current type
#check (x : ℝ)  -- Verify coercion works

Pattern 3: Function application

-- If f : ℝ → ℝ and n : ℕ
f ↑n    -- Apply after coercion
f (n : ℝ)  -- Explicit

Pattern 4: Bypass coercion unification with calc

When automatic coercion (π/6 : Real.Angle) won't unify with explicit ((π/6 : ℝ) : Real.Angle), use calc chain with coercion-free middle steps:

calc ((Real.pi / 6 : ℝ) : Real.Angle)
    = ∠ A C H := by rw [← h_angle]  -- Explicit coercion matches helper signature
  _ = ∠ A C B := by simp [h_eq]      -- Pure angle equality (no coercion!)
  _ = ((4 * Real.pi / 9 : ℝ) : Real.Angle) := by rw [angle_ACB]

4. Tactic 'exact' Failed

Full error message:

tactic 'exact' failed, type mismatch
  term
has type
  A → B
but is expected to have type
  ∀ x, A x → B x

What it means: The term's type is close but not exactly the goal type.

Solutions:

Solution 1: Use apply instead

-- exact doesn't work but apply might
apply my_lemma
-- Leaves subgoals to fill

Solution 2: Restructure term

-- Wrong order
exact ⟨h.1, h.2⟩  -- Type mismatch

-- Correct order
exact ⟨h.2, h.1⟩  -- Works

Solution 3: Add intermediate steps

-- Instead of: exact complex_term
have h1 := part1
have h2 := part2
exact ⟨h1, h2⟩

5. Unknown Identifier (Missing Tactic or Namespace Open)

Full error message:

unknown identifier 'ring'
unknown identifier 'Tendsto'

What it means: Tactic not imported OR namespace not opened.

Cause 1: Missing tactic import

Common missing imports:

import Mathlib.Tactic.Ring          -- ring, ring_nf
import Mathlib.Tactic.Linarith      -- linarith, nlinarith
import Mathlib.Tactic.FieldSimp     -- field_simp
import Mathlib.Tactic.Continuity    -- continuity
import Mathlib.Tactic.Measurability -- measurability
import Mathlib.Tactic.Positivity    -- positivity

Quick fix: 1. See error for tactic name 2. Add import Mathlib.Tactic.TacticName 3. Rebuild

Cause 2: Missing `open` declarations

Names like Tendsto and atTop live in the Filter namespace. Without opening it, Lean cannot resolve them:

-- ❌ WRONG: bare identifiers without open
have h : Tendsto f atTop (𝓝 x) := ...

-- ✅ CORRECT: open the relevant namespaces
open Filter Topology in
have h : Tendsto f atTop (𝓝 x) := ...

Alternatively, you can fully qualify the names (Filter.Tendsto, Filter.atTop), but open Filter Topology is the standard mathlib practice.

6. Equation Compiler Failed (Termination)

Full error message:

fail to show termination for
  my_recursive_function
with errors
  ...

What it means: Lean can't automatically prove the function terminates.

Solutions:

Pattern 1: Add termination_by clause

def my_rec (n : ℕ) : ℕ :=
  if n = 0 then 0
  else my_rec (n - 1)
termination_by n  -- Decreasing argument

Pattern 2: Well-founded recursion

def my_rec (l : List α) : Result :=
  match l with
  | [] => base_case
  | h :: t => combine h (my_rec t)
termination_by l.length

Pattern 3: Use sorry for termination proof

def my_rec (x : X) : Y := ...
termination_by measure_func x
decreasing_by sorry  -- TODO: Prove later

7. Unsolved Goals (Nat.pos_of_ne_zero and Arithmetic)

Full error message:

unsolved goals
h : m ≠ 0
h2 : (4 : ℝ) / ε ≤ ↑m
⊢ False

What it means: After introducing a contradiction hypothesis, the goal is False but the tactic can't derive the contradiction.

Common scenario: Proving m > 0 from m ≠ 0 and some bound, but norm_num fails because the expressions are symbolic (not concrete numbers).

Why norm_num fails:

• norm_num works on concrete numerical expressions (like 2 + 2 = 4)
• When you have symbolic variables like 4/ε, norm_num can't evaluate them
• After rw [h] where h : m = 0, you get 4/ε ≤ 0, but norm_num can't derive False from this

Solution: Use simp to eliminate variables, then linarith

-- ❌ WRONG: norm_num can't solve symbolic arithmetic
have hm_pos' : m > 0 := Nat.pos_of_ne_zero (by
  intro h
  rw [h] at h2  -- Now h2 : 4/ε ≤ 0
  norm_num at h2  -- FAILS: can't derive False because 4/ε is symbolic
  )
-- Error: unsolved goals ⊢ False

-- ✅ CORRECT: simp eliminates the variable, then linarith
have hm_pos' : m > 0 := Nat.pos_of_ne_zero (by
  intro h
  simp [h] at h2  -- Now h2 : 4/ε ≤ 0 AND we eliminated m entirely
  have : (4 : ℝ) / ε > 0 := by positivity  -- Explicit positivity proof
  linarith)  -- Can now derive contradiction: 0 < 4/ε ≤ 0

Key insight:

• norm_num = numerical normalization (concrete numbers)
• simp = simplification (eliminates variables, unfolds definitions)
• linarith = linear arithmetic solver (works with inequalities and symbolic expressions)

General pattern for contradiction proofs: 1. simp [hypothesis] to eliminate the contradictory assumption 2. Establish any needed positivity facts with positivity 3. linarith to derive the contradiction from inequalities

When to use each tactic:

• norm_num: Concrete arithmetic (2 + 2 = 4, 7 < 10)
• simp: Simplify using hypotheses and definitions
• linarith: Linear inequalities with variables (a + b ≤ c, x > 0 → x + 1 > 0)
• omega: Integer linear arithmetic (works on ℕ and ℤ)

8. Unexpected Token/Identifier in Proof (Section Doc Comments)

Full error message:

unexpected identifier; expected command
unexpected token 'have'; expected command

What it means: Section doc comments /-! ... -/ in tactic mode can terminate proof parsing.

CRITICAL: Section doc comments terminate proof context, causing everything after to be interpreted as top-level declarations.

-- ❌ WRONG: Section comments break proof
lemma my_proof := by
  classical
  set mW := ... with hmW

  /-! ### Step 0: documentation -/

  set φp := ... with hφp  -- ERROR: unexpected identifier
  have h := ...           -- ERROR: unexpected token 'have'

-- ✅ CORRECT: Use regular comments
lemma my_proof := by
  classical
  set mW := ... with hmW
  -- Step 0: documentation
  set φp := ... with hφp  -- ✓ Works
  have h := ...           -- ✓ Works

Best practice: Use -- for in-proof comments, reserve /-! -/ for top-level documentation only.

9. Variable Shadowing in Lambda

Full error message:

type mismatch
  a
has type
  Set ℝ≥0∞
but is expected to have type
  α

What it means: Lambda variable shadows outer variable, causing type confusion.

-- ❌ WRONG: 'a' in lambda shadows outer 'a'
have h_sp_le : ∀ n a, (sp n a) ≤ φp a := by
  intro n a
  have := SimpleFunc.iSup_eapprox_apply
    (fun a => ENNReal.ofReal (max (φ a) 0))  -- 'a' shadows!
    ... a  -- ERROR: which 'a'?

-- ✅ CORRECT: Rename lambda variable or add type annotation
have h_sp_le : ∀ n a, (sp n a) ≤ φp a := by
  intro n a
  have := SimpleFunc.iSup_eapprox_apply
    (fun (x : α) => ENNReal.ofReal (max (φ x) 0))
    ... a  -- ✓ Clear: outer 'a'

Prevention: Use different variable names in nested lambdas or add explicit type annotations.

10. No Goals After Tactic

Full error message:

no goals to be solved

What it means: Previous tactic already completed the proof, but another tactic remains.

-- ❌ WRONG: simp already solved goal
have hφp_nn : ∀ a, 0 ≤ φp a := by
  intro a
  simp [φp]
  exact le_max_right _ _  -- ERROR: no goals left

-- ✅ CORRECT: Remove redundant tactic
have hφp_nn : ∀ a, 0 ≤ φp a := by
  intro a
  simp [φp]  -- ✓ simp completes proof

Debug: Check goal state after each tactic. If "no goals" appears, proof is done.

Quick Debug Workflow

When encountering any error:

1. Read error location carefully - Often points to exact issue 2. Use #check - Verify types of all terms involved 3. Simplify - Try to create minimal example that fails 4. Search mathlib - Error might be documented in lemma comments 5. Ask Zulip - Lean community is very helpful

Quick Checklist for "Unexpected" Errors in Proofs

When facing "unexpected identifier/token" in long proofs:

1. ☐ Search for /-! ... -/ section comments → replace with -- 2. ☐ Check for bare identifiers (Tendsto, atTop) → open Filter Topology 3. ☐ Look for lambda shadowing → rename variables or add type annotations 4. ☐ Check for "no goals" after simp → remove redundant tactics 5. ☐ For section variables + explicit params → rely on section, use (by infer_instance) 6. ☐ For sub-σ-algebra work → ensure hmW_le : mW ≤ _ proof exists

---

Additional Common Errors

9. Dot Notation Namespace Confusion

Error message:

type mismatch
  expected Filter
  got Measure

What it means: You're using dot notation for a lemma name that conflicts with a type constructor.

Example:

-- ❌ WRONG: Interpreted as EventuallyEq constructor call
have := h.EventuallyEq.comp_measurePreserving
--        ^ EventuallyEq constructor called with μ as first argument
--          Expected Filter but got Measure

Solution: Use snake_case standalone names instead of dot notation:

-- ✅ CORRECT: Call the lemma function
have := EventuallyEq.comp_measurePreserving h ...

Pattern: If you see type errors where:

• A Measure is expected to be a Filter
• A Set is expected to be a different type
• "Expected X but got Y" for completely unrelated types

Check if you're using dot notation for a lemma that shares a name with a type constructor.

Rule: For private helper lemmas extending common type names (EventuallyEq, Tendsto, Continuous, etc.), use standalone function call syntax, not dot notation.

10. Numerals in Propositional Contexts

Error message:

numerals are data but expected type is Prop

What it means: You're passing a value (numeral) where a proof term is expected.

Example:

-- ❌ WRONG: 1 is a numeral (data), not a proof
have := h1.atTop_add 1
--                    ^ Expected: Tendsto proof
--                      Got: numeral 1

Solution: For constant function limits, use tendsto_const_nhds:

-- ✅ CORRECT: Pass a proof term
have := h1.atTop_add (tendsto_const_nhds : Tendsto (fun _ => (1 : ℝ)) atTop (nhds 1))

Pattern: Functions like atTop_add work on limits and need proof terms:

• Tendsto f atTop (nhds a) ← This is a Prop (needs proof)
• 1 ← This is data (ℕ or ℝ)

Common fixes:

-- For constant functions
tendsto_const_nhds : Tendsto (fun _ => c) filter (nhds c)

-- For simple expressions
use lemmas like Filter.tendsto_id, Filter.tendsto_const_pure

11. Error Location Can Be Misleading

Problem: Lean reports errors where elaboration fails, not always where the mistake is.

Example:

error: type mismatch at line 4238

But the actual mistake is at line 4231.

Why: Elaborator processes code sequentially and reports failure at the point where it can't continue, which may be several lines after the actual error.

Strategy:

When investigating an error: 1. Read 5-10 lines before the reported location 2. Look for recent changes (especially new let bindings, have statements, or tactic calls) 3. Check for missing hypotheses or incorrect variable names 4. Verify that all previous lines actually compile in isolation

Example workflow:

-- Error reported at line 4238
-- Start reading from line 4228-4230

-- Line 4231: Ah! Wrong variable name here
let μX := pathLaw μ X  -- Should be Y not X

-- Lines 4232-4237: These all assumed μX was correct
-- Line 4238: Where elaboration finally failed

Pattern: The mistake is often in:

• Most recent let or have before error (wrong RHS)
• Most recent tactic (applied wrong lemma)
• Missing hypothesis from 2-5 lines before

Don't: Assume the error line is where you need to fix. Do: Trace backwards from error to find the root cause.

12. Alpha/Beta-Equivalence Issues (Binder Mismatches)

Problem: Lean fails to match expressions because binder names differ (α-equivalence) or beta-redexes aren't reduced.

Error message:

tactic 'simp' failed
  binder x doesn't match goal's binder ω

Example failure:

have h := integral_condExp (f := fun ω => μ[g|m] ω * ξ ω)
-- h : ∫ (x : Ω), F x ∂μ = ∫ (x : Ω), μ[F|m] x ∂μ
-- Goal: ∫ (ω : Ω), μ[g|m] ω * ξ ω ∂μ = ...

simpa using h.symm  -- Error: binder x ≠ binder ω

Why it fails: Lean doesn't automatically recognize that fun x => F x and fun ω => F ω are the same when comparing goal to hypothesis.

Solution: Use `set ... with` pattern to name expression once

-- Name the integrand once and for all
set F : Ω → ℝ := fun ω => μ[g | m] ω * ξ ω with hF

-- Apply lemma to named function F
have h_goal :
    ∫ (ω : Ω), μ[g | m] ω * ξ ω ∂μ
  = ∫ (ω : Ω), μ[(fun ω => μ[g | m] ω * ξ ω) | m] ω ∂μ := by
  simpa [hF] using
    (MeasureTheory.integral_condExp (μ := μ) (m := m) (hm := hm) (f := F)).symm

exact h_goal.symm

Why this works:

• set F := ... gives the expression an explicit name
• Lean never compares different lambda expressions
• simpa [hF] unfolds F uniformly in both places
• No binder name mismatches because we use the same name throughout

Pattern: 1. set F := <complex expr> with hF 2. Apply lemma to the named F 3. Unfold with simpa [hF] or rw [hF]

See also: lean-phrasebook.md - "Name complex expression to avoid alpha/beta-equivalence issues"

---

Type Class Debugging Commands

-- See synthesis trace
set_option trace.Meta.synthInstance true in
theorem test : Goal := by apply_instance

-- See which instance was chosen
#check (inferInstance : IsProbabilityMeasure μ)

-- Check all implicit arguments
#check @my_lemma

Common Patterns to Avoid

❌ Fighting the Type Checker

-- Repeatedly trying variations until something compiles
exact h
exact h.1
exact ⟨h⟩
exact (h : _)  -- Guessing

✅ Understanding Then Fixing

#check h  -- See what h actually is
#check goal  -- See what's needed
-- Now fix systematically

❌ Ignoring Error Messages

-- "It says type mismatch, let me try random things"

✅ Reading Carefully

-- Error says "has type A but expected B"
-- Solution: Convert A to B or restructure

---

OOM from Large Dependent Type Signatures

A file with all-sorry proof bodies can still OOM or take tens of minutes to build if the type signatures are expensive to elaborate. sorry skips the proof, but Lean must still fully elaborate every type signature at the definition site and every call site that destructures the result; importing or downstream files can also become slow or time out.

Watch for this when:

• Return type has 6+ existential/conjunction components with dependent types
• Types reference List/Vector/Array with length-indexed proof terms
• Types contain Fin.cast, by omega, or by simp; omega inside binder types
• File takes minutes to build even though all proofs are sorry

Symptom: lake build consumes multi-GB RAM and is OOM-killed (exit code 137), or LSP times out on any file importing the module.

Fixes: 1. Isolate pathological signatures into small, rarely-recompiled files 2. Break dependency chains — extract structure definitions into lightweight files so editing proof files doesn't trigger re-elaboration of heavy signatures 3. Sorry call sites too — when obtain ⟨...many binders...⟩ := heavy_thm ... is itself expensive, sorry the caller until the callee is ready

Not a concern when: signatures are small (3-4 binders or fewer), types don't have deeply nested proof-term dependencies, or file builds in seconds.

---

Build Log Capture

For debugging persistent build errors, capture the full log for inspection:

Basic Capture

LOG=$(mktemp -t lean4_build_XXXXXX.log)
lake build 2>&1 | tee "$LOG"

# Quick scans
tail -n 120 "$LOG"
rg -n "error|warning|failed" "$LOG"

With Git Hash (Conflict-Safe)

HASH=$(git rev-parse --short HEAD 2>/dev/null || date +%s)
LOG="/tmp/lean4_build_${HASH}_$RANDOM.log"
lake build 2>&1 | tee "$LOG"

Benefits:

• Preserves logs across rebuilds for comparison
• Avoids filename clashes between runs
• Enables grep without rebuilding
• Links log to specific commit state

See also: Repair Mode for escalation-only repair policy.

Compiler-Guided Proof Repair - Quick Reference

Table of Contents

• Philosophy
• Quick Start
• API Discovery Workflow
• Core Workflow
• Repair Strategies by Error Type
• Common Pitfalls
• Error Pattern Recognition
• Key Success Factors
• Expected Outcomes
• Tools Reference
• Common Patterns
• Best Practices
• Troubleshooting

---

Core insight: Use Lean's compiler feedback to drive iterative repair with small, budgeted LLM calls instead of blind best-of-N sampling.

Key principle: Generate → Compile → Diagnose → Fix → Verify (tight loop, K=1)

Inspired by: APOLLO (https://arxiv.org/abs/2505.05758)

---

Philosophy

Traditional Approach (Blind Sampling):

Generate 100 proof attempts → Test all → Pick best
❌ Wasteful: Most attempts fail identically
❌ No learning: Same error repeated many times
❌ Expensive: Large model × high K

Compiler-Guided Approach:

Generate attempt → Lean error → Route to specific fix → Retry (max 24 attempts)
✅ Efficient: Error-driven action selection
✅ Adaptive: Different fix strategies per error type
✅ Economical: Small K (often K=1), fast model first, escalate only when needed
✅ Learning: Log attempts, avoid repeating dead ends

Key wins:

• Low sampling budgets (K=1 or K=3) with compiler guidance beat high-K blind sampling
• Multi-stage approach (fast model → escalate to strong model) optimizes cost/quality
• Solver cascade (try automation before resampling) handles many cases mechanically
• Early stopping (bail after 3 identical errors) prevents runaway costs

---

Quick Start

Repair is integrated into /lean4:prove and /lean4:autoprove:

/lean4:prove --repair-only         # Fix build errors only (guided)
/lean4:prove                       # Full workflow (includes repair when needed)

Repair is escalation-only: it triggers when compiler errors are the active blocker and LSP-first tactics cannot resolve them (same blocker 2x, same build error 2x, or 3+ errors). Not the default on first failure. See cycle-engine.md for the full invocation policy.

---

API Discovery Workflow

Core principle: Search before guessing. LeanFinder + LSP tools prevent 80% of API-related errors.

The "LeanFinder First" Rule

Before writing ANY Lean API call:

1. Search with natural language (lean_leanfinder):

   lean_leanfinder(query="Lp space membership predicate measure theory")
   # → Finds: MemLp (not Memℒp, not memLp)

2. Confirm locally (lean_local_search):

   lean_local_search("MemLp", limit=5)
   # → Verify it exists in your imports

3. Check signature (lean_hover_info):

   lean_hover_info(file, line, col)
   # → See: MemLp f p μ (expects ENNReal, not ℝ!)

4. THEN write the code

Why this matters:

• Mathematical notation ≠ Lean API names (ℒp → MemLp, not Memℒp)
• Type signatures have subtle requirements (ENNReal.ofReal 2 vs 2)
• Field vs function matters (x.foo vs Foo.bar x)

Example: Lp Space API Discovery

❌ Wrong (guessing from math notation):

theorem foo (f g : α → ℝ) (h : f =ᵐ[μ] g) : f ∈ Memℒp 2 μ := by
  exact h.memLp  -- Multiple errors: Memℒp doesn't exist, memLp is not a field, 2 has wrong type

✅ Correct (LeanFinder → hover → verify):

theorem foo (f g : α → ℝ) (hf : MemLp f (ENNReal.ofReal 2) μ) (h : f =ᵐ[μ] g) :
    MemLp g (ENNReal.ofReal 2) μ := by
  exact MemLp.ae_eq hf h.symm  -- Correct API name, correct type, correct direction

How LeanFinder helped: 1. Query: "Lp space membership predicate" → Found MemLp (not Memℒp) 2. Hover on MemLp → Saw signature expects ENNReal for p parameter 3. Local search: "ae_eq" → Found MemLp.ae_eq takes f =ᵐ[μ] g (not g =ᵐ[μ] f)

---

Core Workflow

1. Compile → Extract Error

lake env lean FILE.lean 2> errors.txt   # run from project root
python3 $LEAN4_SCRIPTS/parse_lean_errors.py errors.txt > context.json

Extracts: error type, location, goal state, local context, code snippet

2. Try Solver Cascade (many simple cases, free!)

python3 $LEAN4_SCRIPTS/solver_cascade.py context.json FILE.lean

Tries in order: rfl → simp → ring → linarith → nlinarith → omega → exact? → apply? → grind → aesop

If any succeeds → apply diff, recompile

3. Agent Repair (if cascade fails)

Stage 1 (fast): First 6 attempts

• Approach: Quick, pattern-based fixes
• Temperature: 0.2, K=1
• Budget: ~2s per attempt
• Strategy: Quick, obvious fixes

Stage 2 (strong, precise): After Stage 1 exhausted or complex errors

• Approach: Strategic reasoning with global context
• Temperature: 0.1, K=1
• Budget: ~10s per attempt
• Strategy: Deep analysis, global context

Escalation triggers:

• Same error 3 times in Stage 1
• Error types: synth_instance, recursion_depth, timeout
• Stage 1 attempts exhausted

4. Apply Patch → Recompile

git apply patch.diff
lake env lean FILE.lean   # run from project root

If success → done! If fail → next iteration (max 24 attempts)

Cycle-level budget: The 24-attempt internal limit is the agent ceiling. Within prove/autoprove, tighter cycle budgets apply: max 2 per error signature, max 6 (prove) or 8 (autoprove) per cycle. No improvement after 2 consecutive attempts on same signature → stuck.

---

Repair Strategies by Error Type

type_mismatch

Strategies: 1. convert _ using N (N = unification depth 1-3) 2. Explicit type annotation: (expr : TargetType) 3. refine with placeholders 4. rw to align types 5. Intermediate have with correct type

Example:

-  exact h
+  convert continuous_of_measurable h using 2
+  simp

unsolved_goals

Strategies: 1. Try automation: simp?, apply?, exact?, grind, aesop 2. By goal shape:

• Equality → rfl, ring, linarith
• ∀ → intro
• ∃ → use or refine ⟨_, _⟩
• → → intro then conclusion

3. Search mathlib for lemma 4. Break down: constructor, cases, induction

Example:

-  sorry
+  intro x
+  apply lemma_from_mathlib
+  exact h

unknown_ident

Strategies: 1. Use LeanFinder FIRST: lean_leanfinder(query="natural language description of what you want") 2. Check for ASCII vs Unicode naming (ℒp → MemLp, not Memℒp) 3. Search locally: lean_local_search("ident", limit=10) 4. Add namespace: open Foo or open scoped Bar 5. Add import: import Mathlib.Foo.Bar 6. Check for typo

Example:

+import Mathlib.Topology.Instances.Real
 ...
-  continuous_real
+  Real.continuous

Why LeanFinder first:

• Mathematical notation ≠ API names (use natural language instead)
• Finds correct spelling and namespace immediately
• Much faster than trial-and-error with imports

synth_implicit / synth_instance

Strategies: 1. Provide instance: haveI : Instance := ... 2. Local instance: letI : Instance := ... 3. Open scope: open scoped Topology 4. Reorder arguments (instances before regular params)

Example:

+  haveI : MeasurableSpace β := inferInstance
   apply theorem_needing_instance

sorry_present

Strategies: 1. Search mathlib (many already exist) 2. Automated solvers (cascade handles this) 3. Compositional proof from mathlib lemmas 4. Break into subgoals

timeout / recursion_depth

Strategies: 1. Narrow simp: simp only [lem1, lem2] not simp [*] 2. Clear unused: clear h1 h2 3. Replace decide with native_decide 4. Provide instances explicitly 5. Revert then re-intro in better order

Example:

-  simp [*]
+  simp only [foo_lemma, bar_lemma]

---

Common Pitfalls

Pitfall 1: Type Coercion Assumptions (ENNReal vs ℝ)

The trap: In Lean 4, 2 and ENNReal.ofReal 2 are not interchangeable, even though mathematically they represent the same value.

❌ What fails:

-- Lp spaces expect ENNReal for the p parameter
theorem bar (f : α → ℝ) : MemLp f 2 μ := by  -- ❌ Type mismatch: expected ENNReal, got ℕ
  ...

✅ What works:

theorem bar (f : α → ℝ) : MemLp f (ENNReal.ofReal 2) μ := by  -- ✓ Correct type
  ...

How to catch this: 1. Use lean_goal to see expected type 2. Check API signature with lean_hover_info 3. Look for ENNReal, ℝ≥0∞, or ℝ≥0 in type signature

General pattern: Measure theory APIs often expect:

• ENNReal (ℝ≥0∞) for measures, Lp norms
• ℝ≥0 (NNReal) for nonnegative reals
• ℝ for signed reals

Don't assume automatic coercion—check the signature!

Pitfall 2: Field Access vs Function Call

The trap: Coming from other languages, x.foo and Foo.bar x seem equivalent, but in Lean they're different.

❌ What fails:

theorem baz (f : α → ℝ) (hf : MemLp f p μ) : Prop := by
  have := hf.memLp  -- ❌ Invalid field 'memLp', type MemLp doesn't have a field named memLp
  ...

✅ What works:

theorem baz (f g : α → ℝ) (hf : MemLp f p μ) (h : f =ᵐ[μ] g) : MemLp g p μ := by
  exact MemLp.ae_eq hf h.symm  -- ✓ Function call, not field access
  ...

How to catch this: 1. Error message: "Invalid field 'X'" → It's a function, not a field 2. Use lean_hover_info on the identifier to see if it's a field or function 3. Use lean_local_search to find the correct namespace (e.g., MemLp.ae_eq not hf.ae_eq)

Rule of thumb:

• Fields: Data stored in a structure (e.g., point.x, σ.carrier)
• Functions: Operations on types (e.g., MemLp.ae_eq, Continuous.comp)

Pitfall 3: Almost Everywhere Equality Direction

The trap: =ᵐ[μ] has directionality. Lemmas expect specific order.

❌ What fails:

theorem qux (hf : MemLp f p μ) (h : g =ᵐ[μ] f) : MemLp g p μ := by
  exact MemLp.ae_eq hf h  -- ❌ Type mismatch: expected f =ᵐ[μ] g, got g =ᵐ[μ] f

✅ What works:

theorem qux (hf : MemLp f p μ) (h : g =ᵐ[μ] f) : MemLp g p μ := by
  exact MemLp.ae_eq hf h.symm  -- ✓ Reverse with .symm

How to catch this: 1. Error: "Type mismatch" with EventuallyEq → Check direction 2. Use lean_goal to see expected f =ᵐ[μ] g vs actual g =ᵐ[μ] f 3. Use .symm to reverse direction

General pattern: Many equivalence relations have .symm:

• =ᵐ[μ] (EventuallyEq)
• ≈ (equivalence)
• ↔ (iff)
• = (equality - though usually inferred)

Pitfall 4: ASCII vs Unicode Naming

The trap: Mathematical notation uses Unicode (ℒp), but Lean APIs use ASCII (MemLp).

❌ What fails:

import Mathlib.MeasureTheory.Function.LpSpace

theorem foo : Memℒp f p μ := by  -- ❌ Unknown identifier 'Memℒp'
  ...

✅ What works:

import Mathlib.MeasureTheory.Function.LpSpace

theorem foo : MemLp f p μ := by  -- ✓ ASCII name
  ...

How to catch this: 1. Error: "Unknown identifier" with Unicode → Try ASCII equivalent 2. Use lean_leanfinder with natural language: "Lp space membership" 3. Check mathlib documentation for canonical names

Common translations:

• ℒp → MemLp (Lp space membership)
• ∞ → infinity or top (⊤)
• ≥0 → NNReal or ENNReal
• ∫ → integral

---

Error Pattern Recognition

Quick diagnosis guide: Match error message to likely cause and fix strategy.

"Invalid field 'X'"

Likely cause: Trying to use function call syntax on a type that doesn't have that field.

Fix strategy: 1. Use lean_hover_info to check if it's a function 2. Change x.foo to Foo.bar x 3. Use lean_local_search to find correct namespace

Example:

-  have := hf.memLp
+  have := MemLp.ae_eq hf h

"Type mismatch: expected ENNReal, got ℕ" (or ℝ)

Likely cause: Missing ENNReal.ofReal or ENNReal.ofNat coercion.

Fix strategy: 1. Check if API expects ENNReal (use lean_hover_info) 2. Wrap numeric literals: 2 → ENNReal.ofReal 2 3. For variables: p → ENNReal.ofReal p (if p : ℝ)

Example:

-  theorem bar : MemLp f 2 μ := by
+  theorem bar : MemLp f (ENNReal.ofReal 2) μ := by

"Application type mismatch" with EventuallyEq

Likely cause: Wrong direction for =ᵐ[μ] argument.

Fix strategy: 1. Use lean_goal to see expected direction 2. Add .symm to reverse: h.symm 3. Check lemma signature with lean_hover_info

Example:

-  exact MemLp.ae_eq hf h
+  exact MemLp.ae_eq hf h.symm

"Unknown identifier 'X'"

Likely cause: Unicode name, missing import, or wrong namespace.

Fix strategy: 1. Try LeanFinder FIRST: lean_leanfinder(query="natural language description") 2. Check for ASCII equivalent (Memℒp → MemLp) 3. Search locally: lean_local_search("X") 4. Add import if found externally 5. Check for typo

Example:

-  exact Memℒp.ae_eq
+  exact MemLp.ae_eq  -- ASCII, not Unicode

"Failed to synthesize instance"

Likely cause: Missing type class instance in context.

Fix strategy: 1. Add instance: haveI : Instance := inferInstance 2. Or: letI : Instance := ... 3. Check import: may need import Mathlib.X.Y 4. Reorder parameters (instances before regular params)

Example:

+  haveI : MeasurableSpace α := inferInstance
   apply theorem_needing_instance

---

Key Success Factors

Low Sampling Budgets

• K=1 per attempt (not K=100)
• Strong compiler feedback guides next attempt
• Efficient iteration to success

Solver-First Strategy

• Many errors solved by automation
• Zero LLM cost for simple cases
• Only escalate to agent when needed

Multi-Stage Escalation

• Fast model for most cases
• Strong model only when needed
• Cost-effective repair process

Early Stopping

• Bail after 3 identical errors
• Prevents runaway costs
• Max 24 attempts total

Structured Logging

• Every attempt logged to .repair/attempts.ndjson
• Track: error hash, stage, solver success, elapsed time
• Learn successful patterns over time

---

Expected Outcomes

Success improves over time as structured logging enables learning from repair attempts.

Efficiency benefits:

• Solver cascade handles many simple cases mechanically (zero LLM cost)
• Multi-stage escalation: fast model first, strong model only when needed
• Early stopping prevents runaway attempts on intractable errors
• Low sampling budget (K=1) with strong compiler feedback

Cost optimization:

• Solver cascade: Free (automated tactics)
• Stage 1 (fast): Low cost, handles most common cases
• Stage 2 (strong): Higher cost, reserved for complex cases
• Much more cost-effective than blind best-of-N sampling

---

Tools Reference

Error parsing:

python3 $LEAN4_SCRIPTS/parse_lean_errors.py errors.txt

Solver cascade:

python3 $LEAN4_SCRIPTS/solver_cascade.py context.json FILE.lean

Via prove/autoprove:

/lean4:prove --repair-only         # Repair mode (guided)
/lean4:prove                       # Full workflow with repair

Search (LSP preferred):

lean_leansearch("description")     # Natural language
lean_loogle("type pattern")        # Type-based

Fallback scripts:

bash $LEAN4_SCRIPTS/smart_search.sh "query" --source=all

---

Common Patterns

Pattern 1: Type Mismatch with convert

Before:

theorem foo (h : Measurable f) : Continuous f := by
  exact h  -- ❌ type mismatch

After:

theorem foo (h : Measurable f) : Continuous f := by
  convert continuous_of_measurable h using 2
  simp

Pattern 2: Missing Instance with haveI

Before:

theorem bar : Property := by
  apply lemma  -- ❌ failed to synthesize instance

After:

theorem bar : Property := by
  haveI : MeasurableSpace α := inferInstance
  apply lemma

Pattern 3: Unknown Identifier → Import

Before:

theorem baz : Result := by
  exact Continuous.comp  -- ❌ unknown identifier

After:

import Mathlib.Topology.Basic

theorem baz : Result := by
  exact Continuous.comp

Pattern 4: Unsolved Goal → Automation

Before:

theorem qux : a + b = b + a := by
  sorry  -- ❌

After:

theorem qux : a + b = b + a := by
  ring  -- ✓ (found by solver cascade)

---

Best Practices

1. Build After Every Fix (Most Important!)

Rule: Build after EVERY 1-2 fixes, not after "a batch of fixes."

Why:

• One error at a time is faster than five errors at once
• Immediate feedback prevents cascading errors
• Errors compound—fixing one may introduce another
• Fast iteration loop beats careful batch processing

Anti-pattern:

# ❌ BAD: Make many changes, then build
fix error 1
fix error 2
fix error 3
lake build  # Now you have errors from all three fixes mixing together!

Better pattern:

# ✅ GOOD: Verify after each fix
# Per-edit: lean_diagnostic_messages(file) for immediate feedback
# File gate: lake env lean FILE.lean after each fix (run from project root)
# Milestone: lake build only at checkpoint
fix error 1  # → lean_diagnostic_messages(file) → lake env lean FILE.lean
fix error 2  # → lean_diagnostic_messages(file) → lake env lean FILE.lean
fix error 3  # → lean_diagnostic_messages(file) → lake env lean FILE.lean

With LSP (even better):

# After each edit, immediate verification:
lean_diagnostic_messages(file_path)
lean_goal(file_path, line)

2. LeanFinder First, Always

Before writing ANY API call: 1. lean_leanfinder(query="natural language") 2. lean_local_search("result") 3. lean_hover_info to check signature 4. THEN write code

Prevents: Wrong API names, wrong type signatures, wrong argument order.

3. Start with Solver Cascade

Always try automated solvers before LLM. Many cases succeed with zero cost.

4. Search Mathlib First

Many proofs already exist. Use search tools before generating novel proofs.

5. Minimal Diffs

Change only 1-5 lines. Preserve existing proof structure and style.

6. Trust the Loop

Don't overthink individual attempts. The loop will iterate. Fast attempts beat perfect attempts.

7. Learn from Logs

Review .repair/attempts.ndjson to see what strategies worked. Build intuition over time.

---

Troubleshooting

Repair loop stuck on same error:

• Check if error is truly at fault line
• Run /lean4:prove with "every change" review cadence to see attempts
• May need manual intervention

Agent generates wrong fixes:

• Fast approaches optimize for speed → may miss context
• Use /lean4:prove with conservative approach for better understanding
• Or fix manually and continue

Solver cascade too aggressive:

• Some proofs need structure, not automation
• Fix manually and continue with /lean4:prove

Cost concerns:

• Solver cascade is free (use it!)
• Stage 1 (fast) very low cost
• Early stopping prevents runaway costs
• Much more cost-effective than blind sampling

---

False Statement Handling

When repair loop fails repeatedly:

• Consider the statement may be false
• Try explicit counterexample search on small domains
• If found, create counterexample lemma instead of continuing repair
• See prove/autoprove stuck → salvage workflow

---

Compiler-guided repair inspired by APOLLO (https://arxiv.org/abs/2505.05758) Word count: ~1100

Profiling Workflows

Scope: Not part of the prove/autoprove default loop. Consulted when diagnosing slow Lean builds or proofs.

Version metadata:

- Verified on: Lean reference + release notes through v4.27.0

- Last validated: 2026-02-17

- Confidence: medium (docs reviewed; snippets not batch-compiled)

When to Use

• A file or lemma is slow to elaborate or compile
• A tactic is timing out or producing long traces
• You need hotspots before refactoring

Composable Profiling Blocks

• Scope: set options near the slow section
• Target: build a single module with lake build +My.Module
• Threshold: raise/lower trace.profiler.threshold
• Clock: use useHeartbeats when wall-clock noise is high
• Output: write JSON to inspect in Firefox Profiler

Quick Setup

set_option trace.profiler true
set_option trace.profiler.threshold 200
-- optional:
-- set_option trace.profiler.useHeartbeats true
-- set_option trace.profiler.output "/tmp/lean-profile.json"
-- set_option trace.profiler.output.pp true

Notes:

• Threshold is in milliseconds unless useHeartbeats is true
• If trace.profiler.output is set, Lean writes Firefox Profiler JSON and suppresses stdout traces

Workflow

1. Narrow scope: add profiling options near the slow section 2. Build a single target: lake build +My.Module 3. If noisy, increase trace.profiler.threshold 4. If wall-clock noise is high, enable useHeartbeats 5. If using JSON output, open in Firefox Profiler and inspect hot traces 6. Iterate by shrinking scope or adding local reductions to isolate the hotspot

What to Record

• The slowest trace entries and surrounding lemmas
• Whether the slowdown is elaboration, simp, or typeclass search
• Any change in performance after narrowing scope

See Also

• performance-optimization.md — optimization patterns (irreducible wrappers, simp budgets)