lean4-theorem-proving
Systematic approach to developing formal proofs in Lean 4, managing sorries, using mathlib, and building verified mathematics
View on GitHubTable of content
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 - Specialized agents for batch proof optimization
- lean4-memories - Persistent learning across sessions (requires MCP)
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
…(truncated)