Systematic approach to developing formal proofs in Lean 4, managing sorries, using mathlib, and building verified mathematics
Installation
npx claude-plugins install @cameronfreer/lean4-theorem-proving-skills/lean4-theorem-proving
Contents
Folders: commands, config, docs, hooks, scripts, skills, tests
Files: COMMANDS.md, FUTURE-FEATURES.md, README.md
Documentation
Systematic workflows for Lean 4 proof development.
What You Get
- Lean LSP integration - Sub-second feedback vs 30s builds
- 8 slash commands - Build, fill sorries, repair proofs, golf, check axioms, refactor
- 16 automation scripts - Search, analysis, verification, refactoring
- Reference guides - Tactics, mathlib patterns, domain-specific workflows
Installation
/plugin marketplace add cameronfreer/lean4-skills
/plugin install lean4-theorem-proving
See INSTALLATION.md for manual installation and LSP setup.
Commands
| Command | Purpose |
|---|---|
/build-lean | Build with formatted error analysis |
/fill-sorry [file:line] | Fill a sorry interactively |
/repair-file [file] | Compiler-guided repair of entire file |
/repair-interactive | Interactive step-by-step proof repair |
/golf-proofs [file] | Optimize proofs (30-40% reduction) |
/check-axioms [file] | Verify axiom hygiene |
/analyze-sorries | Scan project for incomplete proofs |
/search-mathlib [query] | Find mathlib lemmas |
/refactor-have [file] | Inline or extract have-blocks |
/clean-warnings | Clean linter warnings by category |
Automation Scripts
Search: search_mathlib.sh, smart_search.sh, find_instances.sh, find_usages.sh
Analysis: proof_complexity.sh, dependency_graph.sh, build_profile.sh, suggest_tactics.sh
Verification: sorry_analyzer.py, check_axioms.sh, check_axioms_inline.sh, simp_lemma_tester.sh
Quality: pre_commit_hook.sh, unused_declarations.sh, minimize_imports.py, proof_templates.sh
See scripts/README.md for documentation.
Reference Guides
| Guide | Content |
|---|---|
| lean-phrasebook.md | Math English to Lean |
| mathlib-guide.md | Search, imports, naming |
| tactics-reference.md | Comprehensive tactics |
| domain-patterns.md | Analysis, algebra, topology |
| measure-theory.md | Conditional expectation |
| compiler-guided-repair.md | APOLLO-inspired repair |
| proof-golfing.md | Proof optimization |
| proof-refactoring.md | Extract helpers |
Key Principles
- Always compile before commit -
lake buildis your test suite - Document every sorry with strategy and dependencies
- Search mathlib first before reproving standard results
- One change at a time - fill one sorry, compile, commit
Optional Add-ons
lean4-subagents- Not included in the current upstream repositorylean4-memories- Not included in the current upstream repository
Bootstrap Hook
On startup, the plugin copies tool scripts to .claude/tools/lean4/ in your workspace. This is read-only and sandboxed.
License
MIT License - see LICENSE
Part of lean4-skills
Included Skills
This plugin includes 1 skill definition:
lean4-theorem-proving
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
View skill definition
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