Use when working with Lean 4 (.lean files), writing mathematical proofs, seeing "failed to synthesize instance" errors, managing sorry/axiom elimination, or searching mathlib for lemmas - provides build-first workflow, haveI/letI patterns, compiler-guided repair, and LSP integration
npxskills add benchflow-ai/skillsbench--skill lean4-theorem-provingLoading…
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.
| 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 |
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.
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.
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.
have statements and documented sorries before writing tacticshaveI/letI when synthesis fails, respect binder order for sub-structuresPhilosophy: 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.
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.
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
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.
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:
rfl → simp → ring → linarith → nlinarith → omega → exact? → apply? → aesoplean4-proof-repair agent:
Key benefits:
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 confirmationsDetailed 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.
| 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.
private or in dedicated sectionsexample for educational code, not lemma/theoremBefore commit:
lake build succeeds on full projectDoing 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).
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
Create or update AgentSkills. Use when designing, structuring, or packaging skills with scripts, references, and assets.
Create or update AgentSkills. Use when designing, structuring, or packaging skills with scripts, references, and assets.
Set up and use 1Password CLI (op). Use when installing the CLI, enabling desktop app integration, signing in (single or multi-account), or reading/injecting/running secrets via op.
CLI to manage emails via IMAP/SMTP. Use `himalaya` to list, read, write, reply, forward, search, and organize emails from the terminal. Supports multiple accounts and message composition with MML (MIME Meta Language).
Create or update AgentSkills. Use when designing, structuring, or packaging skills with scripts, references, and assets.
Create or update AgentSkills. Use when designing, structuring, or packaging skills with scripts, references, and assets.
Set up and use 1Password CLI (op). Use when installing the CLI, enabling desktop app integration, signing in (single or multi-account), or reading/injecting/running secrets via op.
CLI to manage emails via IMAP/SMTP. Use `himalaya` to list, read, write, reply, forward, search, and organize emails from the terminal. Supports multiple accounts and message composition with MML (MIME Meta Language).