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

Quick Reference

/lean

scripts/

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

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

The 4-Phase Workflow

1. Structure Before Solving - Outline proof strategy with

   have

   statements and documented sorries before writing tactics
2. Helper Lemmas First - Build infrastructure bottom-up, extract reusable components as separate lemmas
3. Incremental Filling - Fill ONE sorry at a time, compile after each, commit working code
4. 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

Essential Tactics

Key tactics:

simp only

rw

apply

exact

refine

by_cases

rcases

ext

funext

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

Complete domain guide: domain-patterns.md

Managing Incomplete Proofs

Standard mathlib axioms (acceptable):

Classical.choice

propext

quot.sound

#print axioms theorem_name

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

1. Compile → extract structured error (type, location, goal, context)
2. Try automated solver cascade first (many simple cases handled mechanically, zero LLM cost)
   • Order:

     rfl → simp → ring → linarith → nlinarith → omega → exact? → apply? → aesop

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

haveI : Instance := ...

letI := ...

(x : ℝ)

↑x

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

Reference Files

Core references: lean-phrasebook.md, mathlib-guide.md, tactics-reference.md, compilation-errors.md

Domain-specific: domain-patterns.md, measure-theory.md, instance-pollution.md, calc-patterns.md

Incomplete proofs: sorry-filling.md, axiom-elimination.md

Optimization & refactoring: performance-optimization.md, proof-golfing.md, proof-refactoring.md, mathlib-style.md

Automation: compiler-guided-repair.md, lean-lsp-server.md, lean-lsp-tools-api.md, subagent-workflows.md