lean4-theorem-proving
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
More from cameronfreer/lean4-skills
lean4
Use when editing .lean files, debugging Lean 4 builds (type mismatch, sorry, failed to synthesize instance, axiom warnings, lake build errors), searching mathlib for lemmas, formalizing mathematics in Lean, or learning Lean 4 concepts. Also trigger when the user asks for help with Lean 4, mathlib, or lakefile. Do NOT trigger for Coq/Rocq, Agda, Isabelle, HOL4, Mizar, Idris, Megalodon, or other non-Lean theorem provers.
97lean4-memories
This skill should be used when working on Lean 4 formalization projects to maintain persistent memory of successful proof patterns, failed approaches, project conventions, and user preferences across sessions using MCP memory server integration
9