Lean 4 Theorem Proving

Core Principle

Build incrementally, structure before solving, trust the type checker. Lean's type checker is your test suite.

Success = lake build passes + zero sorries + zero custom axioms. Theorems with sorries/axioms are scaffolding, not results.

Quick Reference

Resource	What You Get	Where to Find
Interactive Commands	10 slash commands for search, analysis, optimization, repair	Type `/lean` in Claude Code (full guide)
Automation Scripts	19 tools for search, verification, refactoring, repair	Plugin `scripts/` directory (scripts/README.md)
Subagents	4 specialized agents for batch tasks (optional)	subagent-workflows.md
LSP Server	30x faster feedback with instant proof state (optional)	lean-lsp-server.md
Reference Files	18 detailed guides (phrasebook, tactics, patterns, errors, repair, performance)	List below

When to Use

Use for ANY Lean 4 development: pure/applied math, program verification, mathlib contributions.

Critical for: Type class synthesis errors, sorry/axiom management, mathlib search, measure theory/probability work.

Tools & Workflows

7 slash commands for search, analysis, and optimization - type /lean in Claude Code. See COMMANDS.md for full guide with examples and workflows.

16 automation scripts for search, verification, and refactoring. See scripts/README.md for complete documentation.

Lean LSP Server (optional) provides 30x faster feedback with instant proof state and parallel tactic testing. See lean-lsp-server.md for setup and workflows.

Subagent delegation (optional, Claude Code users) enables batch automation. See subagent-workflows.md for patterns.

Build-First Principle

ALWAYS compile before committing. Run lake build to verify. "Compiles" ≠ "Complete" - files can compile with sorries/axioms but aren't done until those are eliminated.

The 4-Phase Workflow

Structure Before Solving - Outline proof strategy with have statements and documented sorries before writing tactics
Helper Lemmas First - Build infrastructure bottom-up, extract reusable components as separate lemmas
Incremental Filling - Fill ONE sorry at a time, compile after each, commit working code
Type Class Management - Add explicit instances with haveI/letI when synthesis fails, respect binder order for sub-structures

Finding and Using Mathlib Lemmas

Philosophy: Search before prove. Mathlib has 100,000+ theorems.

Use /search-mathlib slash command, LSP server search tools, or automation scripts. See mathlib-guide.md for detailed search techniques, naming conventions, and import organization.

Essential Tactics

Key tactics: simp only, rw, apply, exact, refine, by_cases, rcases, ext/funext. See tactics-reference.md for comprehensive guide with examples and decision trees.

Domain-Specific Patterns

Analysis & Topology: Integrability, continuity, compactness patterns. Tactics: continuity, fun_prop.

Algebra: Instance building, quotient constructions. Tactics: ring, field_simp, group.

Measure Theory & Probability (emphasis in this skill): Conditional expectation, sub-σ-algebras, a.e. properties. Tactics: measurability, positivity. See measure-theory.md for detailed patterns.

Complete domain guide: domain-patterns.md

Managing Incomplete Proofs

Standard mathlib axioms (acceptable): Classical.choice, propext, quot.sound. Check with #print axioms theorem_name or /check-axioms.

CRITICAL: Sorries/axioms are NOT complete work. A theorem that compiles with sorries is scaffolding, not a result. Document every sorry with concrete strategy and dependencies. Search mathlib exhaustively before adding custom axioms.

When sorries are acceptable: (1) Active work in progress with documented plan, (2) User explicitly approves temporary axioms with elimination strategy.

Not acceptable: "Should be in mathlib", "infrastructure lemma", "will prove later" without concrete plan.

Compiler-Guided Proof Repair

When proofs fail to compile, use iterative compiler-guided repair instead of blind resampling.

Quick repair: /lean4-theorem-proving:repair-file FILE.lean

How it works:

Compile → extract structured error (type, location, goal, context)
Try automated solver cascade first (many simple cases handled mechanically, zero LLM cost)
- Order: rfl → simp → ring → linarith → nlinarith → omega → exact? → apply? → aesop
If solvers fail → call lean4-proof-repair agent:
- Stage 1: Haiku (fast, most common cases) - 6 attempts
- Stage 2: Sonnet (precise, complex cases) - 18 attempts
Apply minimal patch (1-5 lines), recompile, repeat (max 24 attempts)

Key benefits:

Low sampling budget (K=1 per attempt, not K=100)
Error-driven action selection (specific fix per error type, not random guessing)
Fast model first (Haiku), escalate only when needed (Sonnet)
Solver cascade handles simple cases mechanically (zero LLM cost)
Early stopping prevents runaway costs (bail after 3 identical errors)

Expected outcomes: Success improves over time as structured logging enables learning from attempts. Cost optimized through solver cascade (free) and multi-stage escalation.

Commands:

/repair-file FILE.lean - Full file repair
/repair-goal FILE.lean LINE - Specific goal repair
/repair-interactive FILE.lean - Interactive with confirmations

Detailed guide: compiler-guided-repair.md

Inspired by: APOLLO (https://arxiv.org/abs/2505.05758) - compiler-guided repair with multi-stage models and low sampling budgets.

Common Compilation Errors

Error	Fix
"failed to synthesize instance"	Add `haveI : Instance := ...`
"maximum recursion depth"	Provide manually: `letI := ...`
"type mismatch"	Use coercion: `(x : ℝ)` or `↑x`
"unknown identifier"	Add import

See compilation-errors.md for detailed debugging workflows.

Documentation Conventions

Write timeless documentation (describe what code is, not development history)
Don't highlight "axiom-free" status after proofs are complete
Mark internal helpers as private or in dedicated sections
Use example for educational code, not lemma/theorem

Quality Checklist

Before commit:

lake build succeeds on full project
All sorries documented with concrete strategy
No new axioms without elimination plan
Imports minimal

Doing it right: Sorries/axioms decrease over time, each commit completes one lemma, proofs build on mathlib.

Red flags: Sorries multiply, claiming "complete" with sorries/axioms, fighting type checker for hours, monolithic proofs (>100 lines), long have blocks (>30 lines should be extracted as lemmas - see proof-refactoring.md).